more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
authorwenzelm
Mon Mar 17 20:22:04 2014 +0100 (2014-03-17)
changeset 56184a2bd40830593
parent 56177 bfa9dfb722de
child 56185 851c7b05eb92
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
src/Pure/ML/ml_syntax.ML
     1.1 --- a/src/Pure/ML/ml_syntax.ML	Mon Mar 17 14:40:59 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Mon Mar 17 20:22:04 2014 +0100
     1.3 @@ -85,17 +85,17 @@
     1.4  val print_class = print_string;
     1.5  val print_sort = print_list print_class;
     1.6  
     1.7 -fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
     1.8 -  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
     1.9 -  | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
    1.10 +fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg
    1.11 +  | print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg
    1.12 +  | print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg;
    1.13  
    1.14 -fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
    1.15 -  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
    1.16 -  | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
    1.17 -  | print_term (Bound i) = "Bound " ^ print_int i
    1.18 +fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg
    1.19 +  | print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg
    1.20 +  | print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg
    1.21 +  | print_term (Bound i) = "Term.Bound " ^ print_int i
    1.22    | print_term (Abs (s, T, t)) =
    1.23 -      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    1.24 -  | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
    1.25 +      "Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    1.26 +  | print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2);
    1.27  
    1.28  
    1.29  (* toplevel pretty printing *)