author | wenzelm |
Sun, 12 Nov 2000 14:35:41 +0100 | |
changeset 10453 | ad91d022ab4c |
parent 10452 | abeefb0a79ae |
child 10454 | 9ef2f60ebde5 |
--- a/src/Pure/pure_thy.ML Fri Nov 10 19:20:17 2000 +0100 +++ b/src/Pure/pure_thy.ML Sun Nov 12 14:35:41 2000 +0100 @@ -478,7 +478,8 @@ ("TYPE", "'a itself", NoSyn), (Term.dummy_patternN, "'a", Delimfix "'_")] |> Theory.add_modesyntax ("", false) - [("Goal", "prop => prop", Mixfix ("_", [0], 0))] + (("Goal", "prop => prop", Mixfix ("_", [0], 0)) + :: Syntax.pure_appl_syntax) |> local_path |> (#1 oo (add_defs false o map Thm.no_attributes)) [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),