src/Pure/Syntax/syntax.ML
changeset 168 1bf4e2cab673
parent 167 128e122acc89
child 171 ab0f93a291b5
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Nov 29 12:32:42 1993 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Nov 29 13:51:37 1993 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4  
     1.5  (* mk_tables *)
     1.6  
     1.7 -val mk_tables = extend_tables empty_tables;
     1.8 +(* val mk_tables = extend_tables empty_tables; *)
     1.9  
    1.10  (* FIXME *)
    1.11  fun mk_tables (XGram xgram) =
    1.12 @@ -426,7 +426,7 @@
    1.13  val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
    1.14  
    1.15  
    1.16 -(* extend *)  (* FIXME *)
    1.17 +(* extend *)  (* FIXME *) (* FIXME check *)
    1.18  
    1.19  fun old_extend syn read_ty (roots, xconsts, sext) =
    1.20    let
    1.21 @@ -457,10 +457,10 @@
    1.22    end;
    1.23  
    1.24  
    1.25 -fun extend syn read_ty (ex as (_, _, sext)) =
    1.26 -  (case sext of
    1.27 -    Sext {mixfix = [], ...} => new_extend
    1.28 -  | NewSext {mixfix = [], ...} => new_extend
    1.29 +fun extend syn read_ty (ex as (roots, _, sext)) =
    1.30 +  (case (roots, sext) of
    1.31 +    ([], Sext {mixfix = [], ...}) => new_extend
    1.32 +  | ([], NewSext {mixfix = [], ...}) => new_extend
    1.33    | _ => old_extend) syn read_ty ex;
    1.34  
    1.35