op vor infix-Konstruktoren im datatype binding zum besseren Parsen
authorgagern
Sat Mar 26 16:14:17 2005 +0100 (2005-03-26 ago)
changeset 15632bb178a7a69c1
parent 15631 cbee04ce413b
child 15633 741deccec4e3
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
src/Pure/IsaPlanner/focus_term_lib.ML
src/Pure/proofterm.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/IsaPlanner/focus_term_lib.ML	Sat Mar 26 00:01:56 2005 +0100
     1.2 +++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Sat Mar 26 16:14:17 2005 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    type LeafT (* type for other leaf types in term sturcture *)
     1.5  
     1.6    (* the type to be encoded into *)
     1.7 -  datatype TermT = $ of TermT * TermT
     1.8 +  datatype TermT = op $ of TermT * TermT
     1.9      | Abs of string * TypeT * TermT
    1.10      | lf of LeafT
    1.11  
     2.1 --- a/src/Pure/proofterm.ML	Sat Mar 26 00:01:56 2005 +0100
     2.2 +++ b/src/Pure/proofterm.ML	Sat Mar 26 16:14:17 2005 +0100
     2.3 @@ -15,8 +15,8 @@
     2.4       PBound of int
     2.5     | Abst of string * typ option * proof
     2.6     | AbsP of string * term option * proof
     2.7 -   | % of proof * term option
     2.8 -   | %% of proof * proof
     2.9 +   | op % of proof * term option
    2.10 +   | op %% of proof * proof
    2.11     | Hyp of term
    2.12     | PThm of (string * (string * string list) list) * proof * term * typ list option
    2.13     | PAxm of string * term * typ list option
     3.1 --- a/src/Pure/term.ML	Sat Mar 26 00:01:56 2005 +0100
     3.2 +++ b/src/Pure/term.ML	Sat Mar 26 16:14:17 2005 +0100
     3.3 @@ -36,7 +36,7 @@
     3.4      Var of indexname * typ |
     3.5      Bound of int |
     3.6      Abs of string * typ * term |
     3.7 -    $ of term * term
     3.8 +    op $ of term * term
     3.9    structure Vartab : TABLE
    3.10    structure Typtab : TABLE
    3.11    structure Termtab : TABLE