src/HOL/Tools/inductive.ML
changeset 56245 84fc7dfa3cd4
parent 56052 4873054cd1fc
child 56249 0fda98dd2c93
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -258,7 +258,7 @@
     1.4        handle THM _ => thm RS @{thm le_boolD}
     1.5    in
     1.6      (case concl_of thm of
     1.7 -      Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
     1.8 +      Const (@{const_name Pure.eq}, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
     1.9      | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
    1.10      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    1.11        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL