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;