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