1.1 --- a/src/Tools/code/code_thingol.ML	Sat Sep 15 19:27:48 2007 +0200
     1.2 +++ b/src/Tools/code/code_thingol.ML	Sat Sep 15 19:27:50 2007 +0200
     1.3 @@ -22,8 +22,9 @@
     1.4    datatype itype =
     1.5        `%% of string * itype list
     1.6      | ITyVar of vname;
     1.7 +  type const = string * (dict list list * itype list (*types of arguments*))
     1.8    datatype iterm =
     1.9 -      IConst of string * (dict list list * itype list (*types of arguments*))
    1.10 +      IConst of const
    1.11      | IVar of vname
    1.12      | `$ of iterm * iterm
    1.13      | `|-> of (vname * itype) * iterm
    1.14 @@ -58,7 +59,7 @@
    1.15  
    1.16    datatype def =
    1.17        Bot
    1.18 -    | Fun of typscheme * (iterm list * iterm) list
    1.19 +    | Fun of typscheme * ((iterm list * iterm) * thm) list
    1.20      | Datatype of (vname * sort) list * (string * itype list) list
    1.21      | Datatypecons of string
    1.22      | Class of (class * string) list * (vname * (string * itype) list)
    1.23 @@ -66,7 +67,7 @@
    1.24      | Classrel of class * class
    1.25      | Classinst of (class * (string * (vname * sort) list))
    1.26            * ((class * (string * (string * dict list list))) list
    1.27 -        * (string * iterm) list);
    1.28 +        * ((string * const) * thm) list);
    1.29    type code = def Graph.T;
    1.30    type transact;
    1.31    val empty_code: code;
    1.32 @@ -115,8 +116,10 @@
    1.33      `%% of string * itype list
    1.34    | ITyVar of vname;
    1.35  
    1.36 +type const = string * (dict list list * itype list (*types of arguments*))
    1.37 +
    1.38  datatype iterm =
    1.39 -    IConst of string * (dict list list * itype list)
    1.40 +    IConst of const
    1.41    | IVar of vname
    1.42    | `$ of iterm * iterm
    1.43    | `|-> of (vname * itype) * iterm
    1.44 @@ -234,7 +237,7 @@
    1.45  type typscheme = (vname * sort) list * itype;
    1.46  datatype def =
    1.47      Bot
    1.48 -  | Fun of typscheme * (iterm list * iterm) list
    1.49 +  | Fun of typscheme * ((iterm list * iterm) * thm) list
    1.50    | Datatype of (vname * sort) list * (string * itype list) list
    1.51    | Datatypecons of string
    1.52    | Class of (class * string) list * (vname * (string * itype) list)
    1.53 @@ -242,7 +245,7 @@
    1.54    | Classrel of class * class
    1.55    | Classinst of (class * (string * (vname * sort) list))
    1.56          * ((class * (string * (string * dict list list))) list
    1.57 -      * (string * iterm) list);
    1.58 +      * ((string * const) * thm) list);
    1.59  
    1.60  type code = def Graph.T;
    1.61  
    1.62 @@ -308,7 +311,7 @@
    1.63    ) names NONE;
    1.64  
    1.65  fun check_funeqs eqs =
    1.66 -  (fold (fn (pats, _) =>
    1.67 +  (fold (fn ((pats, _), _) =>
    1.68      let
    1.69        val l = length pats
    1.70      in
    1.71 @@ -339,7 +342,7 @@
    1.72            then error "Too many class operations given"
    1.73            else ();
    1.74          fun check_classop (f, _) =
    1.75 -          if AList.defined (op =) inst_classops f
    1.76 +          if AList.defined (op =) (map fst inst_classops) f
    1.77            then () else error ("Missing definition for class operation " ^ quote f);
    1.78          val _ = map check_classop classops;
    1.79        in d end;
    1.80 @@ -403,7 +406,7 @@
    1.81  
    1.82  fun add_eval_def (name, (t, ty)) code =
    1.83    code
    1.84 -  |> Graph.new_node (name, Fun (([], ty), [([], t)]))
    1.85 +  |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
    1.86    |> fold (curry Graph.add_edge name) (Graph.keys code);
    1.87  
    1.88  end; (*struct*)