src/Pure/primitive_defs.ML
changeset 56243 2e10a36b8d46
parent 46218 ecf6375e2abb
child 63038 1fbad761c1ba
--- a/src/Pure/primitive_defs.ML	Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Pure/primitive_defs.ML	Fri Mar 21 12:34:50 2014 +0100
@@ -37,7 +37,7 @@
 
     fun check_arg (Bound _) = true
       | check_arg (Free (x, _)) = not (is_fixed x)
-      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
+      | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
       | check_arg _ = false;
     fun close_arg (Bound _) t = t
       | close_arg x t = Logic.all x t;