1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -310,19 +310,19 @@
     1.4  fun assoc_thm'' thy thmid =
     1.5    case Symbol.explode thmid of
     1.6      "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
     1.7 -  | "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
     1.8 +  | "s"::"y"::"m"::"_"::id => ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
     1.9    | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
    1.10 -  | _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str
    1.11 +  | _ => thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
    1.12  fun assoc_thm' thy (thmid, ct') =
    1.13    (case Symbol.explode thmid of
    1.14      "s"::"y"::"m"::"_"::id => 
    1.15        if hd id = "#" 
    1.16        then mk_thm thy ct'
    1.17 -      else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.18 +      else ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.19    | id =>
    1.20      if hd id = "#" 
    1.21      then mk_thm thy ct'
    1.22 -    else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
    1.23 +    else thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
    1.24    ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 
    1.25      raise ERROR
    1.26        ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")