1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Oct 06 17:03:44 2016 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Oct 10 18:24:14 2016 +0200
     1.3 @@ -318,6 +318,11 @@
     1.4    handle _ => error ("get_rls_scr: no script for " ^ rls');
     1.5  
     1.6  (*Thm.make_thm added to Pure/thm.ML*)
     1.7 +fun mk_thm'' thy t = 
     1.8 +    let val t' = case t of
     1.9 +		     Const ("==>",_) $ _ $ _ => t
    1.10 +		   | _ => Trueprop $ t
    1.11 +    in Thm.make_thm (Thm.global_cterm_of thy t') end;
    1.12  fun mk_thm thy str = 
    1.13      let val t = (Thm.term_of o the o (parse thy)) str
    1.14  	val t' = case t of
    1.15 @@ -410,6 +415,18 @@
    1.16     (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
    1.17     identifiers starting with "#" come from Calc and
    1.18     get a hand-made theorem (containing numerals only).*)
    1.19 +fun assoc_thm'' (thy : theory) ((thmid, term) : thm'') =
    1.20 +  (case Symbol.explode thmid of
    1.21 +    "s"::"y"::"m"::"_"::id => 
    1.22 +      if hd id = "#" 
    1.23 +      then mk_thm'' thy term
    1.24 +      else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.25 +  | id =>
    1.26 +    if hd id = "#" 
    1.27 +    then mk_thm'' thy term
    1.28 +    else thmid |> convert_metaview_to_thmid thy |> num_str
    1.29 +  ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => 
    1.30 +    error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
    1.31  fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
    1.32    (case Symbol.explode thmid of
    1.33      "s"::"y"::"m"::"_"::id =>