src/HOL/Decision_Procs/commutative_ring_tac.ML
changeset 38864 4abe644fcea5
parent 37744 3daaf23b9ab4
child 42361 23f352990944
     1.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4  (* reification of the equation *)
     1.5  val cr_sort = @{sort "comm_ring_1"};
     1.6  
     1.7 -fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
     1.8 +fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
     1.9        if Sign.of_sort thy (T, cr_sort) then
    1.10          let
    1.11            val fs = OldTerm.term_frees eq;