(* this stuff seems to be unnecessary *)
IgenSub = GDT + CI_Rls +
consts
genseqSubst :: "structr => structr => sequent => sequent"
genstrSubst :: "structr => structr => structr => structr"
primrec
"genstrSubst from to (Comma X Y) = (if from = Comma X Y then to else
Comma (genstrSubst from to X) (genstrSubst from to Y))"
(*
"genstrSubst from to (SemiC X Y) = (if from = SemiC X Y then to else
SemiC (genstrSubst from to X) (genstrSubst from to Y))"
"genstrSubst from to (Blob Y) =
(if from = Blob Y then to else Blob (genstrSubst from to Y))"
"genstrSubst from to E = (if from = E then to else E)"
*)
"genstrSubst from to (Star Y) =
(if from = Star Y then to else Star (genstrSubst from to Y))"
"genstrSubst from to I = (if from = I then to else I)"
"genstrSubst from to (SV str) = (if from = (SV str) then to else (SV str))"
"genstrSubst from to (Structform fml) =
(if from = (Structform fml) then to else (Structform fml))"
primrec
genseqSubst_def "genseqSubst from to (Sequent ant suc) =
Sequent (genstrSubst from to ant) (genstrSubst from to suc)"
end