1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 15:31:23 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 18:32:01 2020 +0200
     1.3 @@ -4,10 +4,6 @@
     1.4  
     1.5  signature REWRITE =
     1.6    sig
     1.7 -(*/------- to ThmC_Def -------\*)
     1.8 -    val assoc_thm': theory -> ThmC_Def.thm' -> thm
     1.9 -    val assoc_thm'': theory -> ThmC_Def.thmID -> thm
    1.10 -(*\------- to ThmC_Def -------/*)
    1.11      val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
    1.12      val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
    1.13      val eval_prog_expr: theory -> Rule_Set.T -> term -> term
    1.14 @@ -31,7 +27,6 @@
    1.15      val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
    1.16      val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
    1.17      val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
    1.18 -    val mk_thm: theory -> string -> thm
    1.19      val trace1: int -> string -> unit
    1.20  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.21    end
    1.22 @@ -277,58 +272,6 @@
    1.23  	   handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
    1.24    end;
    1.25  
    1.26 -(* Thm.make_thm added to Pure/thm.ML *)
    1.27 -fun mk_thm thy str = 
    1.28 -  let
    1.29 -    val t = (Thm.term_of o the o (TermC.parse thy)) str
    1.30 -    val t' = case t of
    1.31 -        Const ("Pure.imp", _) $ _ $ _ => t
    1.32 -      | _ => HOLogic.Trueprop $ t
    1.33 -  in Thm.make_thm (Thm.global_cterm_of thy t') end;
    1.34 -
    1.35 -(*/------- to ThmC_Def -------\*)
    1.36 -(* 
    1.37 -  "metaview" as seen from programs and from user input;
    1.38 -  both are parsed as terms by the function package.
    1.39 -*)
    1.40 -fun convert_metaview_to_thmid thy thmid =
    1.41 -  let val thmid' = case thmid of
    1.42 -      "add_commute" => "add.commute"
    1.43 -    | "mult_commute" => "mult.commute"
    1.44 -    | "add_left_commute" => "add.left_commute"
    1.45 -    | "mult_left_commute" => "mult.left_commute"
    1.46 -    | "add_assoc" => "add.assoc"
    1.47 -    | "mult_assoc" => "mult.assoc"
    1.48 -    | _ => thmid
    1.49 -  in (Global_Theory.get_thm thy) thmid' end;
    1.50 -
    1.51 -(* get the theorem associated with the xstring-identifier;
    1.52 -   if the identifier starts with "sym_" then swap lhs = rhs around =
    1.53 -   (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
    1.54 -   identifiers starting with "#" come from Num_Calc and
    1.55 -   get a hand-made theorem (containing numerals only) *)
    1.56 -fun assoc_thm'' thy thmid =
    1.57 -  case Symbol.explode thmid of
    1.58 -    "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
    1.59 -  | "s"::"y"::"m"::"_"::id => ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.60 -  | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
    1.61 -  | _ => thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
    1.62 -fun assoc_thm' thy (thmid, ct') =
    1.63 -  (case Symbol.explode thmid of
    1.64 -    "s"::"y"::"m"::"_"::id => 
    1.65 -      if hd id = "#" 
    1.66 -      then mk_thm thy ct'
    1.67 -      else ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.68 -  | id =>
    1.69 -    if hd id = "#" 
    1.70 -    then mk_thm thy ct'
    1.71 -    else thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
    1.72 -  ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 
    1.73 -    raise ERROR
    1.74 -      ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
    1.75 -(*\------- to ThmC_Def -------/*)
    1.76 -
    1.77 -
    1.78  fun eval_prog_expr thy srls t =
    1.79    let val rew = rewrite_set_ thy false srls t;
    1.80    in case rew of SOME (res,_) => res | NONE => t end;