src/HOL/Nominal/nominal_datatype.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4    end;
     1.5  
     1.6  fun mk_not_sym ths = maps (fn th => case prop_of th of
     1.7 -    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
     1.8 +    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
     1.9    | _ => [th]) ths;
    1.10  
    1.11  fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);