1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Jul 18 21:19:25 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jul 19 15:34:54 2021 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4        (sort |> map quote |> commas |> enclose "List(" ")"))
     1.5  
     1.6  fun scala_of_term (Const (s, T)) =
     1.7 -    enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T)
     1.8 +    enclose "Const (" ")" (quote s ^ ", " ^ scala_of_typ T)
     1.9    | scala_of_term (Free (s, T)) =
    1.10      enclose "Free(" ")" (quote s ^ ", " ^ scala_of_typ T)
    1.11    | scala_of_term (Var ((s, i), T)) =
    1.12 @@ -254,26 +254,26 @@
    1.13  val int_opt_of_string = ThmC_Def.int_opt_of_string
    1.14  fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
    1.15  
    1.16 -fun is_num (Const ("Num.numeral_class.numeral", _) $ _) = true
    1.17 -  | is_num (Const ("Groups.uminus_class.uminus", _) $
    1.18 -    (Const ("Num.numeral_class.numeral", _) $ _)) = true
    1.19 -  | is_num (Const ("Groups.one_class.one", _)) = true
    1.20 -  | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) = true
    1.21 -  | is_num (Const ("Groups.zero_class.zero", _)) = true
    1.22 -  | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.zero_class.zero", _)) = true
    1.23 +fun is_num (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = true
    1.24 +  | is_num (Const (\<^const_name>\<open>uminus\<close>, _) $
    1.25 +    (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) = true
    1.26 +  | is_num (Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
    1.27 +  | is_num (Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
    1.28 +  | is_num (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
    1.29 +  | is_num (Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
    1.30    | is_num _ = false;
    1.31  
    1.32  fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
    1.33  
    1.34 -fun mk_negative T t = Const ("Groups.uminus_class.uminus", T --> T) $ t
    1.35 +fun mk_negative T t = Const (\<^const_name>\<open>uminus\<close>, T --> T) $ t
    1.36  fun mk_frac T (sg, (i1, i2)) =
    1.37    if sg = 1 then
    1.38      if i2 = 1 then HOLogic.mk_number T i1
    1.39 -    else Const ("Rings.divide_class.divide", T --> T --> T) $
    1.40 +    else Const (\<^const_name>\<open>divide_class.divide\<close>, T --> T --> T) $
    1.41        HOLogic.mk_number T i1 $ HOLogic.mk_number T i2
    1.42    else (*take negative*)
    1.43      if i2 = 1 then mk_negative T (HOLogic.mk_number T i1)
    1.44 -    else Const ("Rings.divide_class.divide", T --> T --> T) $
    1.45 +    else Const (\<^const_name>\<open>divide_class.divide\<close>, T --> T --> T) $
    1.46        mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2
    1.47  
    1.48  val numerals_to_Free = (* Makarius 100308 *)
    1.49 @@ -407,7 +407,7 @@
    1.50    | dest_binop_typ _ = raise ERROR "dest_binop_typ: not binary";
    1.51  fun dest_equals (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u)  =  (t, u) (* Pure/logic.ML: Const ("==", ..*)
    1.52    | dest_equals t = raise TERM ("dest_equals'", [t]);
    1.53 -fun is_equality (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _)  =  true  (* logic.ML: Const("=="*)
    1.54 +fun is_equality (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _)  =  true  (* logic.ML: Const ("=="*)
    1.55    | is_equality _ = false;
    1.56  fun mk_equality (t, u) = (Const(\<^const_name>\<open>HOL.eq\<close>, [type_of t, type_of u] ---> HOLogic.boolT) $ t $ u); 
    1.57  fun is_expliceq (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ (Free _) $ _)  =  true
    1.58 @@ -576,16 +576,16 @@
    1.59    |> typ_a2real;       (*TODO drop*)
    1.60  fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
    1.61  
    1.62 -fun is_atom (Const ("Num.numeral_class.numeral", _) $ _) = true
    1.63 -  | is_atom (Const ("Groups.one_class.one", _)) = true
    1.64 -  | is_atom (Const ("Groups.zero_class.zero", _)) = true
    1.65 +fun is_atom (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = true
    1.66 +  | is_atom (Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
    1.67 +  | is_atom (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
    1.68    | is_atom (Const _) = true
    1.69    | is_atom (Free _) = true
    1.70    | is_atom (Var _) = true
    1.71    | is_atom _ = false;
    1.72 -fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = to_string t
    1.73 -  | string_of_atom (t as Const ("Groups.one_class.one", _)) = to_string t
    1.74 -  | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = to_string t
    1.75 +fun string_of_atom (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) = to_string t
    1.76 +  | string_of_atom (t as Const (\<^const_name>\<open>one_class.one\<close>, _)) = to_string t
    1.77 +  | string_of_atom (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = to_string t
    1.78    | string_of_atom (Const (str, _)) = str
    1.79    | string_of_atom (Free (str, _)) = str
    1.80    | string_of_atom (Var ((str, int), _)) = str ^ "_" ^ string_of_int int