1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Oct 31 16:43:48 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Oct 31 16:53:59 2022 +0100
1.3 @@ -76,7 +76,7 @@
1.4 val parseNEW': Proof.context -> string -> term (*old version to be eliminated*)
1.5 val parseNEW'': theory -> string -> term (*old version to be eliminated*)
1.6 (*goal*)val parse: Proof.context -> string -> term
1.7 -(*goal*)val parse_patt: theory -> string -> term (*with typ_a2real still for tests *)
1.8 +(*goal*)val parse_patt: theory -> string -> term
1.9 (*for test/* *)
1.10 (*goal*)val parse_test: Proof.context -> string -> term
1.11 (*goal*)val parse_patt_test: theory -> string -> term
1.12 @@ -527,23 +527,6 @@
1.13 | inst_abs (t1 $ t2) = inst_abs t1 $ inst_abs t2
1.14 | inst_abs t = t;
1.15
1.16 -(* for parse and parse_patt: fix all types to real *)
1.17 -fun T_a2real (Type (s, [])) =
1.18 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
1.19 - | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
1.20 - | T_a2real (TFree (s, srt)) =
1.21 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
1.22 - | T_a2real (TVar (("DUMMY", _), _)) = HOLogic.realT
1.23 - | T_a2real (TVar ((s, i), srt)) =
1.24 - if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TVar ((s, i), srt)
1.25 -(*val typ_a2real: term -> term*)
1.26 -fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T))
1.27 - | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
1.28 - | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
1.29 - | typ_a2real (Bound i) = (Bound i)
1.30 - | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
1.31 - | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
1.32 -
1.33
1.34 (*** parse ***)
1.35
1.36 @@ -562,7 +545,6 @@
1.37 (* to be replaced by parse..*)
1.38 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
1.39 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
1.40 -(*rename to parse_patt..*)
1.41 fun parse_patt thy str = (thy, str)
1.42 |>> Proof_Context.init_global
1.43 |-> Proof_Context.read_term_pattern