# HG changeset patch
# User wenzelm
# Date 1138559025 -3600
# Node ID d32f707893429e8d09043f4648a99c557cf84261
# Parent  577438cc653e971842fb34571723e0124ea3cbad
proper order of trfuns;

diff -r 577438cc653e -r d32f70789342 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Jan 29 19:23:44 2006 +0100
+++ b/src/Pure/pure_thy.ML	Sun Jan 29 19:23:45 2006 +0100
@@ -612,8 +612,6 @@
     ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
   |> Theory.add_modesyntax ("HTML", false)
    [("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
-  |> Theory.add_trfuns Syntax.pure_trfuns
-  |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Theory.add_consts
    [("==", "'a => 'a => prop", InfixrName ("==", 2)),
     ("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
@@ -627,8 +625,8 @@
      Const ("all", (aT --> propT) --> propT),
      Const ("TYPE", a_itselfT),
      Const (Term.dummy_patternN, aT)]
-  |> Theory.add_syntax
-   []
+  |> Theory.add_trfuns Syntax.pure_trfuns
+  |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Sign.local_path
   |> (add_defs_i false o map Thm.no_attributes)
        [("prop_def", Logic.mk_equals (Logic.protect A, A))] |> snd