# HG changeset patch
# User gagern
# Date 1111850057 -3600
# Node ID bb178a7a69c14f9ea4c28578d420053a88ab693e
# Parent  cbee04ce413b61a2188ebc0addd42e263a89dda8
op vor infix-Konstruktoren im datatype binding zum besseren Parsen

diff -r cbee04ce413b -r bb178a7a69c1 src/Pure/IsaPlanner/focus_term_lib.ML
--- a/src/Pure/IsaPlanner/focus_term_lib.ML	Sat Mar 26 00:01:56 2005 +0100
+++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Sat Mar 26 16:14:17 2005 +0100
@@ -34,7 +34,7 @@
   type LeafT (* type for other leaf types in term sturcture *)
 
   (* the type to be encoded into *)
-  datatype TermT = $ of TermT * TermT
+  datatype TermT = op $ of TermT * TermT
     | Abs of string * TypeT * TermT
     | lf of LeafT
 
diff -r cbee04ce413b -r bb178a7a69c1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Mar 26 00:01:56 2005 +0100
+++ b/src/Pure/proofterm.ML	Sat Mar 26 16:14:17 2005 +0100
@@ -15,8 +15,8 @@
      PBound of int
    | Abst of string * typ option * proof
    | AbsP of string * term option * proof
-   | % of proof * term option
-   | %% of proof * proof
+   | op % of proof * term option
+   | op %% of proof * proof
    | Hyp of term
    | PThm of (string * (string * string list) list) * proof * term * typ list option
    | PAxm of string * term * typ list option
diff -r cbee04ce413b -r bb178a7a69c1 src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Mar 26 00:01:56 2005 +0100
+++ b/src/Pure/term.ML	Sat Mar 26 16:14:17 2005 +0100
@@ -36,7 +36,7 @@
     Var of indexname * typ |
     Bound of int |
     Abs of string * typ * term |
-    $ of term * term
+    op $ of term * term
   structure Vartab : TABLE
   structure Typtab : TABLE
   structure Termtab : TABLE