1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -415,18 +415,12 @@
     1.4     (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
     1.5     identifiers starting with "#" come from Calc and
     1.6     get a hand-made theorem (containing numerals only).*)
     1.7 -fun assoc_thm'' (thy : theory) ((thmid, term) : thm'') =
     1.8 -  (case Symbol.explode thmid of
     1.9 -    "s"::"y"::"m"::"_"::id => 
    1.10 -      if hd id = "#" 
    1.11 -      then mk_thm'' thy term
    1.12 -      else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.13 -  | id =>
    1.14 -    if hd id = "#" 
    1.15 -    then mk_thm'' thy term
    1.16 -    else thmid |> convert_metaview_to_thmid thy |> num_str
    1.17 -  ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => 
    1.18 -    error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
    1.19 +fun assoc_thm'' (thy : theory) (thmid : thmID) =
    1.20 +  case Symbol.explode thmid of
    1.21 +    "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
    1.22 +  | "s"::"y"::"m"::"_"::id => ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
    1.23 +  | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
    1.24 +  | _ => thmid |> convert_metaview_to_thmid thy |> num_str
    1.25  fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
    1.26    (case Symbol.explode thmid of
    1.27      "s"::"y"::"m"::"_"::id =>