1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Jul 18 18:30:09 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sun Jul 18 21:15:21 2021 +0200
     1.3 @@ -74,6 +74,7 @@
     1.4    val parseNEW': Proof.context -> string -> term
     1.5    val parseNEW'': theory -> string -> term
     1.6    val parseold: theory -> string -> cterm option
     1.7 +  val parse_strict: theory -> string -> term
     1.8    val parse_patt: theory -> string -> term
     1.9    val perm: term -> term -> bool
    1.10  
    1.11 @@ -322,13 +323,17 @@
    1.12  (* bypass Isabelle's Pretty, which requires ctxt *)
    1.13  fun ids2str t =
    1.14    let
    1.15 -    fun scan vs (Const (s, _)) = if is_num' s then vs else s :: vs
    1.16 +    fun scan vs (t as Const (s, _) $ arg) =
    1.17 +        if is_num t then vs else scan (s :: vs) arg
    1.18 +      | scan vs (Const (s as "Partial_Fractions.AA", _)) = s :: vs (*how get rid of spec.case?*)
    1.19 +      | scan vs (Const _) = vs
    1.20        | scan vs (Free (s, _)) = if is_num' s then vs else s :: vs
    1.21        | scan vs (Var ((s, i), _)) = (s ^ "_" ^ string_of_int i) :: vs
    1.22        | scan vs (Bound _) = vs 
    1.23        | scan vs (Abs (s, _, t)) = scan (s :: vs) t
    1.24        | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
    1.25 -  in ((distinct op =) o (scan [])) t end;
    1.26 +  in ((distinct op =) o (scan [])) t
    1.27 +  end;
    1.28  fun is_bdv str = case Symbol.explode str of "b"::"d"::"v"::_ => true | _ => false;
    1.29  (* instantiate #prop thm with bound variables (as Free) *)
    1.30  fun inst_bdv [] t = t
    1.31 @@ -578,6 +583,13 @@
    1.32    | is_atom (Free _) = true
    1.33    | is_atom (Var _) = true
    1.34    | is_atom _ = false;
    1.35 +fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = to_string t
    1.36 +  | string_of_atom (t as Const ("Groups.one_class.one", _)) = to_string t
    1.37 +  | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = to_string t
    1.38 +  | string_of_atom (Const (str, _)) = str
    1.39 +  | string_of_atom (Free (str, _)) = str
    1.40 +  | string_of_atom (Var ((str, int), _)) = str ^ "_" ^ string_of_int int
    1.41 +  | string_of_atom _ = "DUMMY-string_of_atom";
    1.42  
    1.43  (* from Pure/term.ML; reports if ALL Free's have found a substitution
    1.44     (required for evaluating the preconditions of _incomplete_ models) *)
    1.45 @@ -604,7 +616,9 @@
    1.46  fun op contains_one_of (thm, ids) =
    1.47    Term.exists_Const (fn id => member op= ids id) (Thm.prop_of thm)
    1.48  
    1.49 -fun var_for vs (t as Const (str, _)) id = if id = strip_thy str then t :: vs else vs
    1.50 +fun var_for vs (t as Const (str, _)) id =
    1.51 +    if is_num t then vs
    1.52 +    else if id = strip_thy str then t :: vs else vs
    1.53    | var_for vs (t as Free (str, _)) id = if id = str then t :: vs else vs
    1.54    | var_for vs (t as Var (idn, _)) id = if id = Term.string_of_vname idn then t :: vs else vs
    1.55    | var_for vs (Bound _) _ = vs
    1.56 @@ -614,7 +628,7 @@
    1.57  val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
    1.58    [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
    1.59    \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
    1.60 -  \<^const_name>\<open>powr\<close>],
    1.61 +  \<^const_name>\<open>powr\<close>];
    1.62  (* treat Free, Const, Var as variables in polynomials *)
    1.63  fun vars_of t =
    1.64    let