src/HOL/Tools/inductive.ML
changeset 38864 4abe644fcea5
parent 38665 e92223c886f8
child 39248 4a3747517552
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4    in
     1.5      case concl_of thm of
     1.6        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     1.7 -    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
     1.8 +    | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
     1.9      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    1.10        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    1.11          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))