src/HOL/Tools/datatype_prop.ML
changeset 19233 77ca20b0ed77
parent 17521 0f1c48de39f5
child 20071 8f3e1ddb50e6
--- a/src/HOL/Tools/datatype_prop.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -366,7 +366,7 @@
     val size_consts = map (fn (s, T) =>
       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
 
-    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
+    fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
 
     fun make_size_eqn size_const T (cname, cargs) =
       let