src/HOL/Tools/inductive_set.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 41472 f6ab14e61604
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4  
     1.5  fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
     1.6    case prop_of thm of
     1.7 -    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
     1.8 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
     1.9        (case body_type T of
    1.10           @{typ bool} =>
    1.11             let