1.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -20,8 +20,6 @@
     1.4    val from_rule : Rule.rule -> T
     1.5    val member': id list -> Rule.rule -> bool
     1.6  
     1.7 -  val numerals_to_Free: thm -> thm
     1.8 -
     1.9    val is_sym: id -> bool
    1.10    val thm_from_thy: theory -> ThmC_Def.id -> thm
    1.11  
    1.12 @@ -67,11 +65,6 @@
    1.13    handle ERROR _ => false
    1.14  
    1.15  
    1.16 -(** convert Isabelle's numerals to ISAC's specific format, LEGACY **)
    1.17 -
    1.18 -val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *)
    1.19 -
    1.20 -
    1.21  (** handle symmetric equalities, generated by deriving input terms **)
    1.22  
    1.23  fun is_sym id =
    1.24 @@ -91,11 +84,11 @@
    1.25      "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
    1.26        raise ERROR ("thm_from_thy not impl.for " ^ thmid)
    1.27    | "s" :: "y" :: "m" :: "_" :: id =>
    1.28 -      ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.29 +      ((Global_Theory.get_thm thy) (implode id)) RS sym
    1.30    | "#" :: _ =>
    1.31        raise ERROR ("thm_from_thy not impl.for " ^ thmid)
    1.32    | _ =>
    1.33 -      thmid |> Global_Theory.get_thm thy |> numerals_to_Free
    1.34 +      thmid |> Global_Theory.get_thm thy
    1.35  
    1.36  fun dest_eq_concl thm =
    1.37    (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
    1.38 @@ -179,7 +172,7 @@
    1.39        if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)
    1.40        else Facts.the_single (name, pos) thms;
    1.41      val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);
    1.42 -  in Rule.Thm (xname', numerals_to_Free thm') end;
    1.43 +  in Rule.Thm (xname', thm') end;
    1.44  
    1.45  fun antiquotation binding sym =
    1.46    ML_Antiquotation.value_embedded binding