src/HOL/Tools/inductive_realizer.ML
changeset 36945 9bec62c10714
parent 36744 6e1f3d609a68
child 37136 e0c9d3e49e15
child 37233 b78f31ca4675
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4      [name] => name
     1.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
     1.6  
     1.7 -val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps};
     1.8 +val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
     1.9  
    1.10  fun prf_of thm =
    1.11    let