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