--- 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
--- 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
--- 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