trfuns *after* binder syntax;
authorwenzelm
Tue Nov 20 20:56:42 2001 +0100 (2001-11-20)
changeset 12250c9ff220cb6c7
parent 12249 dd9a51255855
child 12251 53b7962bcdb1
trfuns *after* binder syntax;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Tue Nov 20 20:56:13 2001 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Nov 20 20:56:42 2001 +0100
     1.3 @@ -482,8 +482,6 @@
     1.4    |> Theory.add_nonterminals Syntax.pure_nonterms
     1.5    |> Theory.add_syntax Syntax.pure_syntax
     1.6    |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
     1.7 -  |> Theory.add_trfuns Syntax.pure_trfuns
     1.8 -  |> Theory.add_trfunsT Syntax.pure_trfunsT
     1.9    |> Theory.add_syntax
    1.10     [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
    1.11      (Term.dummy_patternN, "aprop", Delimfix "'_")]
    1.12 @@ -497,6 +495,8 @@
    1.13      (Term.dummy_patternN, "'a", Delimfix "'_")]
    1.14    |> Theory.add_modesyntax ("", false)
    1.15      (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
    1.16 +  |> Theory.add_trfuns Syntax.pure_trfuns
    1.17 +  |> Theory.add_trfunsT Syntax.pure_trfunsT
    1.18    |> local_path
    1.19    |> (#1 oo (add_defs false o map Thm.no_attributes))
    1.20     [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]