diff -r ee78ded1e1ed -r 820bf0840029 test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 13 18:37:24 2020 +0200
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 14 12:39:26 2020 +0200
@@ -17,9 +17,7 @@
 "----------- fun app_rev, Rrls, -------------------------";
 "----------- 2011 thms with axclasses -------------------";
 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
-"----------- fun assoc_thm' -----------------------------";
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
-"----------- fun mk_thm ------------------------------------------------------------------------";
 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
 "--------------------------------------------------------";
@@ -682,27 +680,6 @@
 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
 
 
-"----------- fun assoc_thm' -----------------------------";
-"----------- fun assoc_thm' -----------------------------";
-"----------- fun assoc_thm' -----------------------------";
-val thy = @{theory ProgLang}
-
-val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
-if string_of_thm' thy tth = "6 = 2 * 3" then ()
-else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
-
-val tth = assoc_thm' thy ("add_0_left","");
-if string_of_thm' thy tth = "0 + ?a = ?a" then ()
-else error "assoc_thm' (add_0_left,\"\") changed";
-
-val tth = assoc_thm' thy ("sym_add_0_left","");
-if string_of_thm' thy tth = "?t = 0 + ?t" then ()
-else error "assoc_thm' (sym_add_0_left,\"\") changed";
-
-val tth = assoc_thm' thy ("add_commute","");
-if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
-else error "assoc_thm' (add_commute,\"\") changed"
-
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
@@ -723,72 +700,6 @@
 if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
   else error "Pattern.match CHANGED";
 
-"----------- fun mk_thm ------------------------------------------------------------------------";
-"----------- fun mk_thm ------------------------------------------------------------------------";
-"----------- fun mk_thm ------------------------------------------------------------------------";
-val thy = @{theory Isac_Knowledge}
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-val thm = @{thm realpow_twoI};
-val patt_str = "?r ^^^ 2 = ?r * ?r";
-val term_str = "r ^^^ 2 = r * r";
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-case parse_patt thy patt_str of
-  Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
-      (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
-| _ => error "parse_patt  ?r ^^^ 2 = ?r * ?r  changed";
-case parse thy term_str of
-  NONE => ()
-| _ => writeln "parse does NOT take patterns with '?'";
-
-val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
-if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
-
-val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
-if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
-
-(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
-(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
-  gives a strange thm*);
-(*while this..*) 
-val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
-  ..gives another strange thm; but it is used and works with rewriting: *);
-
-val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
-if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-val thm = @{thm real_mult_div_cancel2};
-val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
-val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-case parse_patt thy patt_str of
-  Const ("Pure.imp", _) $ 
-    (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
-      (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
-        (Const ("HOL.Trueprop", _) $
-          (Const ("HOL.eq", _) $ _ $ _ )) => ()
-| _ => error "parse_patt  ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n  changed";
-case parse thy term_str of
-  NONE => ()
-| _ => writeln "parse does NOT take patterns with '?'";
-
-val t1 = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm);
-if UnparseC.term t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
-
-val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
-if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
-
-(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
-(*and   this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r"  [.]: thm
-  gives a strange thm*);
-(*while this*) 
-val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r"  [.]: thm
-  gives another strange thm; but it is used and words with rewriting: *);
-
-val t1' = (#prop o Thm.rep_thm) (ThmC.numerals_to_Free thm_made);
-if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
-
 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";