clarified codegen interfaces
authorhaftmann
Tue Sep 30 12:49:18 2008 +0200 (2008-09-30)
changeset 284239fc3befd8191
parent 28422 bfa368164502
child 28424 fc6ce1c4d5b7
clarified codegen interfaces
src/HOL/Library/Efficient_Nat.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Sep 30 12:49:17 2008 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Sep 30 12:49:18 2008 +0200
     1.3 @@ -219,17 +219,20 @@
     1.4      then remove_suc_clause thy ths else ths
     1.5    end;
     1.6  
     1.7 -fun lift f thy thms1 =
     1.8 +fun lift f thy eqns1 =
     1.9    let
    1.10 -    val thms2 = Drule.zero_var_indexes_list thms1;
    1.11 -    val thms3 = try (map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    1.12 +    val eqns2 = ((map o apfst) (AxClass.overload thy)
    1.13 +      o burrow_fst Drule.zero_var_indexes_list) eqns1;
    1.14 +    val thms3 = try (map fst
    1.15 +      #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    1.16        #> f thy
    1.17        #> map (fn thm => thm RS @{thm eq_reflection})
    1.18 -      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) thms2;
    1.19 +      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
    1.20      val thms4 = Option.map Drule.zero_var_indexes_list thms3;
    1.21    in case thms4
    1.22     of NONE => NONE
    1.23 -    | SOME thms4 => if Thm.eq_thms (thms2, thms4) then NONE else SOME thms4
    1.24 +    | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
    1.25 +        then NONE else SOME (map (Code_Unit.mk_eqn thy) thms4)
    1.26    end
    1.27  
    1.28  in
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 30 12:49:17 2008 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 30 12:49:18 2008 +0200
     2.3 @@ -449,9 +449,10 @@
     2.4      fun tac thms = Class.intro_classes_tac []
     2.5        THEN ALLGOALS (ProofContext.fact_tac thms);
     2.6      fun get_eq' thy dtco = get_eq thy dtco
     2.7 -      |> map (Code_Unit.constrain_thm [HOLogic.class_eq])
     2.8 +      |> map (Code_Unit.constrain_thm thy [HOLogic.class_eq])
     2.9        |> map Simpdata.mk_eq
    2.10 -      |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]);
    2.11 +      |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}])
    2.12 +      |> map (AxClass.unoverload thy);
    2.13      fun add_eq_thms dtco thy =
    2.14        let
    2.15          val ty = Type (dtco, map TFree vs');
    2.16 @@ -460,7 +461,8 @@
    2.17          val eq_refl = @{thm HOL.eq_refl}
    2.18            |> Thm.instantiate
    2.19                ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
    2.20 -          |> Simpdata.mk_eq;
    2.21 +          |> Simpdata.mk_eq
    2.22 +          |> AxClass.unoverload thy;
    2.23          fun get_thms () = (eq_refl, false)
    2.24            :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
    2.25        in
     3.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 30 12:49:17 2008 +0200
     3.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 30 12:49:18 2008 +0200
     3.3 @@ -122,9 +122,10 @@
     3.4  
     3.5  fun add_typecopy_spec tyco thy =
     3.6    let
     3.7 -    val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
     3.8 -    val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
     3.9 -    val ty = Type (tyco, map TFree vs');
    3.10 +    val SOME { constr, proj_def, inject, vs = raw_vs, ... } = get_info thy tyco;
    3.11 +    val vs = (map o apsnd)
    3.12 +      (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) raw_vs;
    3.13 +    val ty = Type (tyco, map TFree vs);
    3.14      val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr);
    3.15      fun add_def tyco lthy =
    3.16        let
    3.17 @@ -143,12 +144,14 @@
    3.18      fun add_eq_thms thy = 
    3.19        let
    3.20          val eq = inject
    3.21 -          |> Code_Unit.constrain_thm [HOLogic.class_eq]
    3.22 +          |> Code_Unit.constrain_thm thy [HOLogic.class_eq]
    3.23            |> Simpdata.mk_eq
    3.24 -          |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
    3.25 +          |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]
    3.26 +          |> AxClass.unoverload thy;
    3.27          val eq_refl = @{thm HOL.eq_refl}
    3.28            |> Thm.instantiate
    3.29 -              ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []);
    3.30 +              ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
    3.31 +          |> AxClass.unoverload thy;
    3.32        in
    3.33          thy
    3.34          |> Code.add_eqn eq
    3.35 @@ -158,7 +161,7 @@
    3.36      thy
    3.37      |> Code.add_datatype [(constr, ty_constr)]
    3.38      |> Code.add_eqn proj_def
    3.39 -    |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
    3.40 +    |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
    3.41      |> add_def tyco
    3.42      |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
    3.43      #> LocalTheory.exit_global
     4.1 --- a/src/Pure/Isar/code.ML	Tue Sep 30 12:49:17 2008 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Tue Sep 30 12:49:18 2008 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    val del_inline: thm -> theory -> theory
     4.5    val add_post: thm -> theory -> theory
     4.6    val del_post: thm -> theory -> theory
     4.7 -  val add_functrans: string * (theory -> thm list -> thm list option) -> theory -> theory
     4.8 +  val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
     4.9    val del_functrans: string -> theory -> theory
    4.10    val add_datatype: (string * typ) list -> theory -> theory
    4.11    val add_datatype_cmd: string list -> theory -> theory
    4.12 @@ -40,11 +40,11 @@
    4.13    val get_datatype_of_constr: theory -> string -> string option
    4.14    val get_case_data: theory -> string -> (int * string list) option
    4.15    val is_undefined: theory -> string -> bool
    4.16 -  val default_typ: theory -> string -> (string * sort) list * typ
    4.17 +  val default_typscheme: theory -> string -> (string * sort) list * typ
    4.18  
    4.19 -  val preprocess_conv: cterm -> thm
    4.20 +  val preprocess_conv: theory -> cterm -> thm
    4.21    val preprocess_term: theory -> term -> term
    4.22 -  val postprocess_conv: cterm -> thm
    4.23 +  val postprocess_conv: theory -> cterm -> thm
    4.24    val postprocess_term: theory -> term -> term
    4.25  
    4.26    val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory
    4.27 @@ -124,14 +124,13 @@
    4.28  
    4.29  fun certificate thy f r =
    4.30    case Susp.peek r
    4.31 -   of SOME thms => (Susp.value o burrow_fst (f thy)) thms
    4.32 +   of SOME thms => (Susp.value o f thy) thms
    4.33      | NONE => let
    4.34          val thy_ref = Theory.check_thy thy;
    4.35 -      in Susp.delay (fn () => (burrow_fst (f (Theory.deref thy_ref)) o Susp.force) r) end;
    4.36 +      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    4.37  
    4.38 -fun add_drop_redundant (thm, linear) thms =
    4.39 +fun add_drop_redundant thy (thm, linear) thms =
    4.40    let
    4.41 -    val thy = Thm.theory_of_thm thm;
    4.42      val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    4.43      val args = args_of thm;
    4.44      val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
    4.45 @@ -143,9 +142,9 @@
    4.46        else false;
    4.47    in (thm, linear) :: filter_out drop thms end;
    4.48  
    4.49 -fun add_thm _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thm) thms)
    4.50 -  | add_thm true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
    4.51 -  | add_thm false thm (true, thms) = (false, Susp.value [thm]);
    4.52 +fun add_thm thy _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thy thm) thms)
    4.53 +  | add_thm thy true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
    4.54 +  | add_thm thy false thm (true, thms) = (false, Susp.value [thm]);
    4.55  
    4.56  fun add_lthms lthms _ = (false, lthms);
    4.57  
    4.58 @@ -197,7 +196,7 @@
    4.59  datatype thmproc = Thmproc of {
    4.60    pre: MetaSimplifier.simpset,
    4.61    post: MetaSimplifier.simpset,
    4.62 -  functrans: (string * (serial * (theory -> thm list -> thm list option))) list
    4.63 +  functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
    4.64  };
    4.65  
    4.66  fun mk_thmproc ((pre, post), functrans) =
    4.67 @@ -419,25 +418,19 @@
    4.68    end;
    4.69  
    4.70  
    4.71 -
    4.72  (** theorem transformation and certification **)
    4.73  
    4.74 -fun const_of thy = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    4.75 -
    4.76 -fun const_of_eqn thy = AxClass.unoverload_const thy o const_of thy;
    4.77 -
    4.78 -fun common_typ_eqns [] = []
    4.79 -  | common_typ_eqns [thm] = [thm]
    4.80 -  | common_typ_eqns (thms as thm :: _) = (*FIXME is too general*)
    4.81 +fun common_typ_eqns thy [] = []
    4.82 +  | common_typ_eqns thy [thm] = [thm]
    4.83 +  | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*)
    4.84        let
    4.85 -        val thy = Thm.theory_of_thm thm;
    4.86          fun incr_thm thm max =
    4.87            let
    4.88              val thm' = incr_indexes max thm;
    4.89              val max' = Thm.maxidx_of thm' + 1;
    4.90            in (thm', max') end;
    4.91          val (thms', maxidx) = fold_map incr_thm thms 0;
    4.92 -        val ty1 :: tys = map (snd o const_of thy) thms';
    4.93 +        val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms';
    4.94          fun unify ty env = Sign.typ_unify thy (ty1, ty) env
    4.95            handle Type.TUNIFY =>
    4.96              error ("Type unificaton failed, while unifying defining equations\n"
    4.97 @@ -449,90 +442,45 @@
    4.98            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
    4.99        in map (Thm.instantiate (instT, [])) thms' end;
   4.100  
   4.101 -fun certify_const thy const thms =
   4.102 +fun certify_const thy c eqns =
   4.103    let
   4.104 -    fun cert thm = if const = const_of_eqn thy thm
   4.105 -      then thm else error ("Wrong head of defining equation,\nexpected constant "
   4.106 -        ^ Code_Unit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
   4.107 -  in map cert thms end;
   4.108 +    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
   4.109 +      then eqn else error ("Wrong head of defining equation,\nexpected constant "
   4.110 +        ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
   4.111 +  in map cert eqns end;
   4.112  
   4.113 +fun check_linear (eqn as (thm, linear)) =
   4.114 +  if linear then eqn else Code_Unit.bad_thm
   4.115 +    ("Duplicate variables on left hand side of defining equation:\n"
   4.116 +      ^ Display.string_of_thm thm);
   4.117 +
   4.118 +fun mk_eqn thy linear =
   4.119 +  Code_Unit.error_thm ((if linear then check_linear else I) o Code_Unit.mk_eqn thy);
   4.120 +fun mk_liberal_eqn thy = Code_Unit.warning_thm (check_linear o Code_Unit.mk_eqn thy);
   4.121 +fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy);
   4.122 +fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy);
   4.123  
   4.124  
   4.125  (** operational sort algebra and class discipline **)
   4.126  
   4.127  local
   4.128  
   4.129 -fun aggr_neutr f y [] = y
   4.130 -  | aggr_neutr f y (x::xs) = aggr_neutr f (f y x) xs;
   4.131 -
   4.132 -fun aggregate f [] = NONE
   4.133 -  | aggregate f (x::xs) = SOME (aggr_neutr f x xs);
   4.134 -
   4.135 -fun inter_sorts algebra =
   4.136 -  aggregate (map2 (curry (Sorts.inter_sort algebra)));
   4.137 -
   4.138 -fun specific_constraints thy (class, tyco) =
   4.139 +fun arity_constraints thy algebra (class, tyco) =
   4.140    let
   4.141 -    val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
   4.142 -    val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
   4.143 -    val eqns = classparams
   4.144 +    val base_constraints = Sorts.mg_domain algebra tyco [class];
   4.145 +    val classparam_constraints = Sorts.complete_sort algebra [class]
   4.146 +      |> maps (map fst o these o try (#params o AxClass.get_info thy))
   4.147        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
   4.148        |> map (Symtab.lookup ((the_eqns o the_exec) thy))
   4.149        |> (map o Option.map) (map fst o Susp.force o snd)
   4.150        |> maps these
   4.151 -      |> map (Thm.transfer thy);
   4.152 -    fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
   4.153 -      | sorts_of tys = map (snd o dest_TVar) tys;
   4.154 -    val sorts = map (sorts_of o Sign.const_typargs thy o const_of thy) eqns;
   4.155 -  in sorts end;
   4.156 -
   4.157 -fun weakest_constraints thy algebra (class, tyco) =
   4.158 -  let
   4.159 -    val all_superclasses = Sorts.complete_sort algebra [class];
   4.160 -  in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
   4.161 -   of SOME sorts => sorts
   4.162 -    | NONE => Sorts.mg_domain algebra tyco [class]
   4.163 -  end;
   4.164 -
   4.165 -fun strongest_constraints thy algebra (class, tyco) =
   4.166 -  let
   4.167 -    val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class];
   4.168 -    val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses;
   4.169 -  in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
   4.170 -   of SOME sorts => sorts
   4.171 -    | NONE => replicate
   4.172 -        (Sign.arity_number thy tyco) (Sorts.minimize_sort algebra (Sorts.all_classes algebra))
   4.173 -  end;
   4.174 -
   4.175 -fun get_algebra thy (class, tyco) =
   4.176 -  let
   4.177 -    val base_algebra = Sign.classes_of thy;
   4.178 -  in if can (Sorts.mg_domain base_algebra tyco) [class]
   4.179 -    then base_algebra
   4.180 -    else let
   4.181 -      val superclasses = Sorts.super_classes base_algebra class;
   4.182 -      val sorts = inter_sorts base_algebra
   4.183 -          (map_filter (fn class => try (Sorts.mg_domain base_algebra tyco) [class]) superclasses)
   4.184 -        |> the_default (replicate (Sign.arity_number thy tyco) [])
   4.185 -    in
   4.186 -      base_algebra
   4.187 -      |> Sorts.add_arities (Syntax.pp_global thy) (tyco, [(class, sorts)])
   4.188 -    end
   4.189 -  end;
   4.190 -
   4.191 -fun gen_classparam_typ constr thy class (c, tyco) = 
   4.192 -  let
   4.193 -    val algebra = get_algebra thy (class, tyco);
   4.194 -    val cs = these (try (#params o AxClass.get_info thy) class);
   4.195 -    val SOME ty = AList.lookup (op =) cs c;
   4.196 -    val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
   4.197 -      (constr thy algebra (class, tyco));
   4.198 -    val ty_inst = Type (tyco, map TFree sort_args);
   4.199 -  in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
   4.200 +      |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
   4.201 +    val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
   4.202 +  in fold inter_sorts classparam_constraints base_constraints end;
   4.203  
   4.204  fun retrieve_algebra thy operational =
   4.205    Sorts.subalgebra (Syntax.pp_global thy) operational
   4.206 -    (weakest_constraints thy (Sign.classes_of thy))
   4.207 +    (arity_constraints thy (Sign.classes_of thy))
   4.208      (Sign.classes_of thy);
   4.209  
   4.210  in
   4.211 @@ -545,76 +493,6 @@
   4.212      val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
   4.213    in retrieve_algebra thy (member (op =) operational_classes) end;
   4.214  
   4.215 -val classparam_weakest_typ = gen_classparam_typ weakest_constraints;
   4.216 -val classparam_strongest_typ = gen_classparam_typ strongest_constraints;
   4.217 -
   4.218 -fun assert_eqn_linear (eqn as (thm, linear)) =
   4.219 -  if linear then eqn else Code_Unit.bad_thm
   4.220 -    ("Duplicate variables on left hand side of defining equation:\n"
   4.221 -      ^ Display.string_of_thm thm);
   4.222 -
   4.223 -fun assert_eqn_typ (thm, linear) =
   4.224 -  let
   4.225 -    val thy = Thm.theory_of_thm thm;
   4.226 -    fun check_typ_classparam tyco (c, thm) =
   4.227 -          let
   4.228 -            val SOME class = AxClass.class_of_param thy c;
   4.229 -            val (_, ty) = const_of thy thm;
   4.230 -            val ty_decl = classparam_weakest_typ thy class (c, tyco);
   4.231 -            val ty_strongest = classparam_strongest_typ thy class (c, tyco);
   4.232 -            fun constrain thm = 
   4.233 -              let
   4.234 -                val max = Thm.maxidx_of thm + 1;
   4.235 -                val ty_decl' = Logic.incr_tvar max ty_decl;
   4.236 -                val (_, ty') = const_of thy thm;
   4.237 -                val (env, _) = Sign.typ_unify thy (ty_decl', ty') (Vartab.empty, max);
   4.238 -                val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
   4.239 -                  cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
   4.240 -              in Thm.instantiate (instT, []) thm end;
   4.241 -          in if Sign.typ_instance thy (ty_strongest, ty)
   4.242 -            then if Sign.typ_instance thy (ty, ty_decl)
   4.243 -            then thm
   4.244 -            else (warning ("Constraining type\n" ^ Code_Unit.string_of_typ thy ty
   4.245 -              ^ "\nof defining equation\n"
   4.246 -              ^ Display.string_of_thm thm
   4.247 -              ^ "\nto permitted most general type\n"
   4.248 -              ^ Code_Unit.string_of_typ thy ty_decl);
   4.249 -              constrain thm)
   4.250 -            else Code_Unit.bad_thm ("Type\n" ^ Code_Unit.string_of_typ thy ty
   4.251 -              ^ "\nof defining equation\n"
   4.252 -              ^ Display.string_of_thm thm
   4.253 -              ^ "\nis incompatible with permitted least general type\n"
   4.254 -              ^ Code_Unit.string_of_typ thy ty_strongest)
   4.255 -          end;
   4.256 -    fun check_typ_fun (c, thm) =
   4.257 -      let
   4.258 -        val (_, ty) = const_of thy thm;
   4.259 -        val ty_decl = Sign.the_const_type thy c;
   4.260 -      in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   4.261 -        then thm
   4.262 -        else Code_Unit.bad_thm ("Type\n" ^ Code_Unit.string_of_typ thy ty
   4.263 -           ^ "\nof defining equation\n"
   4.264 -           ^ Display.string_of_thm thm
   4.265 -           ^ "\nis incompatible with declared function type\n"
   4.266 -           ^ Code_Unit.string_of_typ thy ty_decl)
   4.267 -      end;
   4.268 -    fun check_typ (c, thm) =
   4.269 -      case AxClass.inst_of_param thy c
   4.270 -       of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
   4.271 -        | NONE => check_typ_fun (c, thm);
   4.272 -    val c = const_of_eqn thy thm;
   4.273 -    val thm' = check_typ (c, thm);
   4.274 -  in (thm', linear) end;
   4.275 -
   4.276 -fun mk_eqn linear = Code_Unit.error_thm
   4.277 -  (assert_eqn_typ o (if linear then assert_eqn_linear else I) o Code_Unit.mk_eqn);
   4.278 -val mk_liberal_eqn = Code_Unit.warning_thm
   4.279 -  (assert_eqn_typ o assert_eqn_linear o Code_Unit.mk_eqn);
   4.280 -val mk_syntactic_eqn = Code_Unit.warning_thm
   4.281 -  (assert_eqn_typ o Code_Unit.mk_eqn);
   4.282 -val mk_default_eqn = Code_Unit.try_thm
   4.283 -  (assert_eqn_typ o assert_eqn_linear o Code_Unit.mk_eqn);
   4.284 -
   4.285  end; (*local*)
   4.286  
   4.287  
   4.288 @@ -653,10 +531,10 @@
   4.289  val is_undefined = Symtab.defined o snd o the_cases o the_exec;
   4.290  
   4.291  fun gen_add_eqn linear strict default thm thy =
   4.292 -  case (if strict then SOME o mk_eqn linear else mk_liberal_eqn) thm
   4.293 +  case (if strict then SOME o mk_eqn thy linear else mk_liberal_eqn thy) thm
   4.294     of SOME (thm, _) =>
   4.295          let
   4.296 -          val c = const_of_eqn thy thm;
   4.297 +          val c = Code_Unit.const_eqn thm;
   4.298            val _ = if strict andalso (is_some o AxClass.class_of_param thy) c
   4.299              then error ("Rejected polymorphic equation for overloaded constant:\n"
   4.300                ^ Display.string_of_thm thm)
   4.301 @@ -667,7 +545,7 @@
   4.302              else ();
   4.303          in
   4.304            (map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default
   4.305 -            (c, (true, Susp.value [])) (add_thm default (thm, linear))) thy
   4.306 +            (c, (true, Susp.value [])) (add_thm thy default (thm, linear))) thy
   4.307          end
   4.308      | NONE => thy;
   4.309  
   4.310 @@ -676,12 +554,9 @@
   4.311  val add_default_eqn = gen_add_eqn true false true;
   4.312  val add_nonlinear_eqn = gen_add_eqn false true false;
   4.313  
   4.314 -fun del_eqn thm thy = case mk_syntactic_eqn thm
   4.315 - of SOME (thm, _) => let
   4.316 -        val c = const_of_eqn thy thm;
   4.317 -      in map_exec_purge (SOME [c]) (map_eqns
   4.318 -        (Symtab.map_entry c (del_thm thm))) thy
   4.319 -      end
   4.320 +fun del_eqn thm thy = case mk_syntactic_eqn thy thm
   4.321 + of SOME (thm, _) => let val c = Code_Unit.const_eqn thm
   4.322 +      in map_exec_purge (SOME [c]) (map_eqns (Symtab.map_entry c (del_thm thm))) thy end
   4.323    | NONE => thy;
   4.324  
   4.325  fun del_eqns c = map_exec_purge (SOME [c])
   4.326 @@ -689,9 +564,8 @@
   4.327  
   4.328  fun add_eqnl (c, lthms) thy =
   4.329    let
   4.330 -    val lthms' = certificate thy (fn thy => certify_const thy c) lthms;
   4.331 -      (*FIXME must check compatibility with sort algebra;
   4.332 -        alas, naive checking results in non-termination!*)
   4.333 +    val lthms' = certificate thy
   4.334 +      (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
   4.335    in
   4.336      map_exec_purge (SOME [c])
   4.337        (map_eqns (Symtab.map_default (c, (true, Susp.value []))
   4.338 @@ -739,21 +613,12 @@
   4.339  val map_pre = map_exec_purge NONE o map_thmproc o apfst o apfst;
   4.340  val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd;
   4.341  
   4.342 -fun add_inline thm thy = (map_pre o MetaSimplifier.add_simp)
   4.343 -  (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
   4.344 -    (*fully applied in order to get right context for mk_rew!*)
   4.345 -
   4.346 -fun del_inline thm thy = (map_pre o MetaSimplifier.del_simp)
   4.347 -  (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
   4.348 -    (*fully applied in order to get right context for mk_rew!*)
   4.349 +fun gen_add_del_pre_post f thm thy = f thm thy;
   4.350  
   4.351 -fun add_post thm thy = (map_post o MetaSimplifier.add_simp)
   4.352 -  (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
   4.353 -    (*fully applied in order to get right context for mk_rew!*)
   4.354 -
   4.355 -fun del_post thm thy = (map_post o MetaSimplifier.del_simp)
   4.356 -  (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
   4.357 -    (*fully applied in order to get right context for mk_rew!*)
   4.358 +val add_inline = gen_add_del_pre_post (map_pre o MetaSimplifier.add_simp);
   4.359 +val del_inline = gen_add_del_pre_post (map_pre o MetaSimplifier.del_simp);
   4.360 +val add_post = gen_add_del_pre_post (map_post o MetaSimplifier.add_simp);
   4.361 +val del_post = gen_add_del_pre_post (map_post o MetaSimplifier.del_simp);
   4.362    
   4.363  fun add_functrans (name, f) =
   4.364    (map_exec_purge NONE o map_thmproc o apsnd)
   4.365 @@ -784,20 +649,14 @@
   4.366  
   4.367  local
   4.368  
   4.369 -fun apply_functrans thy [] = []
   4.370 -  | apply_functrans thy (thms as (thm, _) :: _) =
   4.371 -      let
   4.372 -        val const = const_of_eqn thy thm;
   4.373 -        val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   4.374 -          o the_thmproc o the_exec) thy;
   4.375 -        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) (map fst thms);
   4.376 -        val thms'' = certify_const thy const thms';
   4.377 -      in map Code_Unit.add_linear thms'' end;
   4.378 +fun apply_functrans thy c _ [] = []
   4.379 +  | apply_functrans thy c [] eqns = eqns
   4.380 +  | apply_functrans thy c functrans eqns = eqns
   4.381 +      |> perhaps (perhaps_loop (perhaps_apply functrans))
   4.382 +      |> map (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
   4.383 +      |> certify_const thy c;
   4.384  
   4.385 -fun rhs_conv conv thm =
   4.386 -  let
   4.387 -    val thm' = (conv o Thm.rhs_of) thm;
   4.388 -  in Thm.transitive thm thm' end
   4.389 +fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   4.390  
   4.391  fun term_of_conv thy f =
   4.392    Thm.cterm_of thy
   4.393 @@ -806,24 +665,27 @@
   4.394    #> Logic.dest_equals
   4.395    #> snd;
   4.396  
   4.397 -in
   4.398 -
   4.399 -fun preprocess thy thms =
   4.400 +fun preprocess thy functrans c eqns =
   4.401    let
   4.402      val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   4.403    in
   4.404 -    thms
   4.405 -    |> apply_functrans thy
   4.406 +    eqns
   4.407 +    |> apply_functrans thy c functrans
   4.408      |> (map o apfst) (Code_Unit.rewrite_eqn pre)
   4.409 -    (*FIXME - must check here: rewrite rule, defining equation, proper constant *)
   4.410 -    |> (map o apfst) (AxClass.unoverload thy)
   4.411 -    |> burrow_fst common_typ_eqns
   4.412 +    |> map (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
   4.413 +    |> burrow_fst (common_typ_eqns thy)
   4.414    end;
   4.415  
   4.416 +fun get_eqns thy c =
   4.417 +  Symtab.lookup ((the_eqns o the_exec) thy) c
   4.418 +  |> Option.map (Susp.force o snd)
   4.419 +  |> these
   4.420 +  |> (map o apfst) (Thm.transfer thy);
   4.421  
   4.422 -fun preprocess_conv ct =
   4.423 +in
   4.424 +
   4.425 +fun preprocess_conv thy ct =
   4.426    let
   4.427 -    val thy = Thm.theory_of_cterm ct;
   4.428      val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   4.429    in
   4.430      ct
   4.431 @@ -831,11 +693,10 @@
   4.432      |> rhs_conv (AxClass.unoverload_conv thy)
   4.433    end;
   4.434  
   4.435 -fun preprocess_term thy = term_of_conv thy preprocess_conv;
   4.436 +fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
   4.437  
   4.438 -fun postprocess_conv ct =
   4.439 +fun postprocess_conv thy ct =
   4.440    let
   4.441 -    val thy = Thm.theory_of_cterm ct;
   4.442      val post = (Simplifier.theory_context thy o #post o the_thmproc o the_exec) thy;
   4.443    in
   4.444      ct
   4.445 @@ -843,43 +704,33 @@
   4.446      |> rhs_conv (Simplifier.rewrite post)
   4.447    end;
   4.448  
   4.449 -fun postprocess_term thy = term_of_conv thy postprocess_conv;
   4.450 -
   4.451 -end; (*local*)
   4.452 -
   4.453 -fun default_typ_proto thy c = case AxClass.inst_of_param thy c
   4.454 - of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
   4.455 -      (c, tyco) |> SOME
   4.456 -  | NONE => (case AxClass.class_of_param thy c
   4.457 -     of SOME class => SOME (Term.map_type_tvar
   4.458 -          (K (TVar ((Name.aT, 0), [class]))) (Sign.the_const_type thy c))
   4.459 -      | NONE => get_constr_typ thy c);
   4.460 +fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
   4.461  
   4.462 -local
   4.463 -
   4.464 -fun get_eqns thy const =
   4.465 -  Symtab.lookup ((the_eqns o the_exec) thy) const
   4.466 -  |> Option.map (Susp.force o snd)
   4.467 -  |> these
   4.468 -  |> (map o apfst) (Thm.transfer thy);
   4.469 -
   4.470 -in
   4.471 -
   4.472 -fun these_eqns thy const =
   4.473 +fun these_eqns thy c =
   4.474    let
   4.475 +    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   4.476 +      o the_thmproc o the_exec) thy;
   4.477      val drop_refl = filter_out
   4.478        (is_equal o Term.fast_term_ord o Logic.dest_equals o Thm.plain_prop_of o fst);
   4.479    in
   4.480 -    get_eqns thy const
   4.481 -    |> preprocess thy
   4.482 +    get_eqns thy c
   4.483 +    |> preprocess thy functrans c
   4.484      |> drop_refl
   4.485    end;
   4.486  
   4.487 -fun default_typ thy c = case default_typ_proto thy c
   4.488 - of SOME ty => Code_Unit.typscheme thy (c, ty)
   4.489 -  | NONE => (case get_eqns thy c
   4.490 -     of (thm, _) :: _ => snd (Code_Unit.head_eqn (AxClass.unoverload thy thm))
   4.491 -      | [] => Code_Unit.typscheme thy (c, Sign.the_const_type thy c));
   4.492 +fun default_typscheme thy c = let
   4.493 +    val typscheme = curry (Code_Unit.typscheme thy) c
   4.494 +    val the_const_type = snd o dest_Const o TermSubst.zero_var_indexes
   4.495 +      o curry Const "" o Sign.the_const_type thy;
   4.496 +  in case AxClass.class_of_param thy c
   4.497 +   of SOME class => the_const_type c
   4.498 +        |> Term.map_type_tvar (K (TVar ((Name.aT, 0), [class])))
   4.499 +        |> typscheme
   4.500 +    | NONE => (case get_constr_typ thy c
   4.501 +       of SOME ty => typscheme ty
   4.502 +        | NONE => (case get_eqns thy c
   4.503 +           of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
   4.504 +            | [] => typscheme (the_const_type c))) end;
   4.505  
   4.506  end; (*local*)
   4.507  
     5.1 --- a/src/Pure/Isar/code_unit.ML	Tue Sep 30 12:49:17 2008 +0200
     5.2 +++ b/src/Pure/Isar/code_unit.ML	Tue Sep 30 12:49:18 2008 +0200
     5.3 @@ -15,8 +15,8 @@
     5.4  
     5.5    (*typ instantiations*)
     5.6    val typscheme: theory -> string * typ -> (string * sort) list * typ
     5.7 -  val inst_thm: sort Vartab.table -> thm -> thm
     5.8 -  val constrain_thm: sort -> thm -> thm
     5.9 +  val inst_thm: theory -> sort Vartab.table -> thm -> thm
    5.10 +  val constrain_thm: theory -> sort -> thm -> thm
    5.11  
    5.12    (*constant aliasses*)
    5.13    val add_const_alias: thm -> theory -> theory
    5.14 @@ -36,16 +36,17 @@
    5.15      -> string * ((string * sort) list * (string * typ list) list)
    5.16  
    5.17    (*defining equations*)
    5.18 -  val assert_rew: thm -> thm
    5.19 -  val mk_rew: thm -> thm
    5.20 -  val add_linear: thm -> thm * bool
    5.21 -  val mk_eqn: thm -> thm * bool
    5.22 -  val head_eqn: thm -> string * ((string * sort) list * typ)
    5.23 -  val expand_eta: int -> thm -> thm
    5.24 +  val assert_eqn: theory -> thm -> thm
    5.25 +  val mk_eqn: theory -> thm -> thm * bool
    5.26 +  val assert_linear: thm * bool -> thm * bool
    5.27 +  val const_eqn: thm -> string
    5.28 +  val const_typ_eqn: thm -> string * typ
    5.29 +  val head_eqn: theory -> thm -> string * ((string * sort) list * typ)
    5.30 +  val expand_eta: theory -> int -> thm -> thm
    5.31    val rewrite_eqn: simpset -> thm -> thm
    5.32    val rewrite_head: thm list -> thm -> thm
    5.33 -  val norm_args: thm list -> thm list 
    5.34 -  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list
    5.35 +  val norm_args: theory -> thm list -> thm list 
    5.36 +  val norm_varnames: theory -> (string -> string) -> (string -> string) -> thm list -> thm list
    5.37  
    5.38    (*case certificates*)
    5.39    val case_cert: thm -> string * (int * string list)
    5.40 @@ -81,9 +82,8 @@
    5.41      val vs = map dest (Sign.const_typargs thy (c, ty));
    5.42    in (vs, ty) end;
    5.43  
    5.44 -fun inst_thm tvars' thm =
    5.45 +fun inst_thm thy tvars' thm =
    5.46    let
    5.47 -    val thy = Thm.theory_of_thm thm;
    5.48      val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    5.49      val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
    5.50      fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
    5.51 @@ -93,9 +93,8 @@
    5.52      val insts = map_filter mk_inst tvars;
    5.53    in Thm.instantiate (insts, []) thm end;
    5.54  
    5.55 -fun constrain_thm sort thm =
    5.56 +fun constrain_thm thy sort thm =
    5.57    let
    5.58 -    val thy = Thm.theory_of_thm thm;
    5.59      val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort
    5.60      val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    5.61      fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v)
    5.62 @@ -103,9 +102,8 @@
    5.63      val insts = map mk_inst tvars;
    5.64    in Thm.instantiate (insts, []) thm end;
    5.65  
    5.66 -fun expand_eta k thm =
    5.67 +fun expand_eta thy k thm =
    5.68    let
    5.69 -    val thy = Thm.theory_of_thm thm;
    5.70      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    5.71      val (head, args) = strip_comb lhs;
    5.72      val l = if k = ~1
    5.73 @@ -153,19 +151,19 @@
    5.74  val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
    5.75  val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
    5.76  
    5.77 -fun norm_args thms =
    5.78 +fun norm_args thy thms =
    5.79    let
    5.80      val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    5.81      val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
    5.82    in
    5.83      thms
    5.84 -    |> map (expand_eta k)
    5.85 +    |> map (expand_eta thy k)
    5.86      |> map (Conv.fconv_rule Drule.beta_eta_conversion)
    5.87    end;
    5.88  
    5.89 -fun canonical_tvars purify_tvar thm =
    5.90 +fun canonical_tvars thy purify_tvar thm =
    5.91    let
    5.92 -    val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm);
    5.93 +    val ctyp = Thm.ctyp_of thy;
    5.94      fun tvars_subst_for thm = (fold_types o fold_atyps)
    5.95        (fn TVar (v_i as (v, _), sort) => let
    5.96              val v' = purify_tvar v
    5.97 @@ -182,9 +180,9 @@
    5.98      val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
    5.99    in Thm.instantiate (inst, []) thm end;
   5.100  
   5.101 -fun canonical_vars purify_var thm =
   5.102 +fun canonical_vars thy purify_var thm =
   5.103    let
   5.104 -    val cterm = Thm.cterm_of (Thm.theory_of_thm thm);
   5.105 +    val cterm = Thm.cterm_of thy;
   5.106      fun vars_subst_for thm = fold_aterms
   5.107        (fn Var (v_i as (v, _), ty) => let
   5.108              val v' = purify_var v
   5.109 @@ -207,7 +205,7 @@
   5.110      val t' = Term.map_abs_vars purify_var t;
   5.111    in Thm.rename_boundvars t t' thm end;
   5.112  
   5.113 -fun norm_varnames purify_tvar purify_var thms =
   5.114 +fun norm_varnames thy purify_tvar purify_var thms =
   5.115    let
   5.116      fun burrow_thms f [] = []
   5.117        | burrow_thms f thms =
   5.118 @@ -217,8 +215,8 @@
   5.119            |> Conjunction.elim_balanced (length thms)
   5.120    in
   5.121      thms
   5.122 -    |> burrow_thms (canonical_tvars purify_tvar)
   5.123 -    |> map (canonical_vars purify_var)
   5.124 +    |> burrow_thms (canonical_tvars thy purify_tvar)
   5.125 +    |> map (canonical_vars thy purify_var)
   5.126      |> map (canonical_absvars purify_var)
   5.127      |> map Drule.zero_var_indexes
   5.128    end;
   5.129 @@ -237,18 +235,16 @@
   5.130        Library.merge (op =) (classes1, classes2));
   5.131  );
   5.132  
   5.133 -fun add_const_alias thm =
   5.134 +fun add_const_alias thm thy =
   5.135    let
   5.136 -    val t = Thm.prop_of thm;
   5.137 -    val thy = Thm.theory_of_thm thm;
   5.138 -    val lhs_rhs = case try Logic.dest_equals t
   5.139 +    val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm)
   5.140       of SOME lhs_rhs => lhs_rhs
   5.141        | _ => error ("Not an equation: " ^ Display.string_of_thm thm);
   5.142      val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
   5.143       of SOME c_c' => c_c'
   5.144        | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm);
   5.145      val some_class = the_list (AxClass.class_of_param thy (snd c_c'));
   5.146 -  in
   5.147 +  in thy |>
   5.148      ConstAlias.map (fn (alias, classes) =>
   5.149        ((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
   5.150    end;
   5.151 @@ -319,9 +315,9 @@
   5.152    in (tyco, (vs, cs''')) end;
   5.153  
   5.154  
   5.155 -(* rewrite theorems *)
   5.156 +(* defining equations *)
   5.157  
   5.158 -fun assert_rew thm =
   5.159 +fun assert_eqn thy thm =
   5.160    let
   5.161      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   5.162        handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
   5.163 @@ -346,34 +342,8 @@
   5.164      val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
   5.165        then ()
   5.166        else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
   5.167 -        ^ Display.string_of_thm thm)
   5.168 -  in thm end;
   5.169 -
   5.170 -fun mk_rew thm =
   5.171 -  let
   5.172 -    val thy = Thm.theory_of_thm thm;
   5.173 -    val ctxt = ProofContext.init thy;
   5.174 -  in
   5.175 -    thm
   5.176 -    |> LocalDefs.meta_rewrite_rule ctxt
   5.177 -    |> assert_rew
   5.178 -  end;
   5.179 -
   5.180 -
   5.181 -(* defining equations *)
   5.182 -
   5.183 -fun add_linear thm =
   5.184 -  let
   5.185 -    val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   5.186 -    val linear = not (has_duplicates (op =)
   5.187 -      ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
   5.188 -  in (thm, linear) end;
   5.189 -
   5.190 -fun assert_eqn thm =
   5.191 -  let
   5.192 -    val thy = Thm.theory_of_thm thm;
   5.193 -    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   5.194 -    val _ = case head of Const _ => () | _ =>
   5.195 +        ^ Display.string_of_thm thm)    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   5.196 +    val (c, ty) = case head of Const c_ty => c_ty | _ =>
   5.197        bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
   5.198      fun check _ (Abs _) = bad_thm
   5.199            ("Abstraction on left hand side of equation\n"
   5.200 @@ -389,25 +359,41 @@
   5.201                 ^ Display.string_of_thm thm)
   5.202            else ();
   5.203      val _ = map (check 0) args;
   5.204 -    val linear = not (has_duplicates (op =)
   5.205 -      ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I ) args []))
   5.206 -  in add_linear thm end;
   5.207 -
   5.208 -val mk_eqn = assert_eqn o mk_rew;
   5.209 +    val ty_decl = Sign.the_const_type thy c;
   5.210 +    val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   5.211 +      then () else bad_thm ("Type\n" ^ string_of_typ thy ty
   5.212 +           ^ "\nof defining equation\n"
   5.213 +           ^ Display.string_of_thm thm
   5.214 +           ^ "\nis incompatible with declared function type\n"
   5.215 +           ^ string_of_typ thy ty_decl)
   5.216 +  in thm end;
   5.217  
   5.218 -fun head_eqn thm =
   5.219 +fun add_linear thm =
   5.220    let
   5.221 -    val thy = Thm.theory_of_thm thm;
   5.222 -    val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals
   5.223 -      o Thm.plain_prop_of) thm;
   5.224 -  in (c, typscheme thy (c, ty)) end;
   5.225 +    val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   5.226 +    val linear = not (has_duplicates (op =)
   5.227 +      ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
   5.228 +  in (thm, linear) end;
   5.229 +
   5.230 +fun assert_linear (thm, false) = (thm, false)
   5.231 +  | assert_linear (thm, true) = if snd (add_linear thm) then (thm, true)
   5.232 +      else bad_thm
   5.233 +        ("Duplicate variables on left hand side of defining equation:\n"
   5.234 +          ^ Display.string_of_thm thm);
   5.235 +
   5.236 +
   5.237 +fun mk_eqn thy = add_linear o assert_eqn thy o AxClass.unoverload thy
   5.238 +  o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   5.239 +
   5.240 +val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   5.241 +val const_eqn = fst o const_typ_eqn;
   5.242 +fun head_eqn thy thm = let val (c, ty) = const_typ_eqn thm in (c, typscheme thy (c, ty)) end;
   5.243  
   5.244  
   5.245  (* case cerificates *)
   5.246  
   5.247  fun case_certificate thm =
   5.248    let
   5.249 -    val thy = Thm.theory_of_thm thm;
   5.250      val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
   5.251        o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
   5.252      val _ = case head of Free _ => true
     6.1 --- a/src/Tools/code/code_funcgr.ML	Tue Sep 30 12:49:17 2008 +0200
     6.2 +++ b/src/Tools/code/code_funcgr.ML	Tue Sep 30 12:49:18 2008 +0200
     6.3 @@ -95,7 +95,7 @@
     6.4              meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs)
     6.5          | NONE => I;
     6.6      val tab = fold meets cs Vartab.empty;
     6.7 -  in map (Code_Unit.inst_thm tab) thms end;
     6.8 +  in map (Code_Unit.inst_thm thy tab) thms end;
     6.9  
    6.10  fun resort_eqnss thy algebra funcgr =
    6.11    let
    6.12 @@ -105,14 +105,14 @@
    6.13        | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
    6.14            then (true, (c, thms))
    6.15            else let
    6.16 -            val (_, (vs, ty)) = Code_Unit.head_eqn thm;
    6.17 +            val (_, (vs, ty)) = Code_Unit.head_eqn thy thm;
    6.18              val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
    6.19 -            val (_, (vs', ty')) = Code_Unit.head_eqn thm'; (*FIXME simplify check*)
    6.20 +            val (_, (vs', ty')) = Code_Unit.head_eqn thy thm'; (*FIXME simplify check*)
    6.21            in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
    6.22      fun resort_recs eqnss =
    6.23        let
    6.24          fun typ_of c = case these (AList.lookup (op =) eqnss c)
    6.25 -         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn) thm
    6.26 +         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn thy) thm
    6.27            | [] => NONE;
    6.28          val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss);
    6.29          val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
    6.30 @@ -158,8 +158,8 @@
    6.31      |> pair (SOME const)
    6.32    else let
    6.33      val thms = Code.these_eqns thy const
    6.34 -      |> burrow_fst Code_Unit.norm_args
    6.35 -      |> burrow_fst (Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var);
    6.36 +      |> burrow_fst (Code_Unit.norm_args thy)
    6.37 +      |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
    6.38      val rhs = consts_of (const, thms);
    6.39    in
    6.40      auxgr
    6.41 @@ -181,8 +181,8 @@
    6.42      val eqnss = raw_eqnss
    6.43        |> resort_eqnss thy algebra funcgr
    6.44        |> filter_out (can (Graph.get_node funcgr) o fst);
    6.45 -    fun typ_eqn c [] = Code.default_typ thy c
    6.46 -      | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn) thm;
    6.47 +    fun typ_eqn c [] = Code.default_typscheme thy c
    6.48 +      | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn thy) thm;
    6.49      fun add_eqns (const, thms) =
    6.50        Graph.new_node (const, (typ_eqn const thms, thms));
    6.51      fun add_deps (eqns as (const, thms)) funcgr =
    6.52 @@ -226,7 +226,7 @@
    6.53      fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
    6.54        t [];
    6.55      val algebra = Code.coregular_algebra thy;
    6.56 -    val thm = Code.preprocess_conv ct;
    6.57 +    val thm = Code.preprocess_conv thy ct;
    6.58      val ct' = Thm.rhs_of thm;
    6.59      val t' = Thm.term_of ct';
    6.60      val consts = map fst (consts_of t');
    6.61 @@ -242,7 +242,7 @@
    6.62      fun evaluator evaluator' thm1 funcgr t =
    6.63        let
    6.64          val thm2 = evaluator' funcgr t;
    6.65 -        val thm3 = Code.postprocess_conv (Thm.rhs_of thm2);
    6.66 +        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
    6.67        in
    6.68          Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
    6.69            error ("could not construct evaluation proof:\n"
     7.1 --- a/src/Tools/code/code_thingol.ML	Tue Sep 30 12:49:17 2008 +0200
     7.2 +++ b/src/Tools/code/code_thingol.ML	Tue Sep 30 12:49:18 2008 +0200
     7.3 @@ -485,7 +485,7 @@
     7.4          val ty = Logic.unvarifyT raw_ty;
     7.5          val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
     7.6            then raw_thms
     7.7 -          else (map o apfst) (Code_Unit.expand_eta 1) raw_thms;
     7.8 +          else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
     7.9        in
    7.10          trns
    7.11          |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
     8.1 --- a/src/Tools/nbe.ML	Tue Sep 30 12:49:17 2008 +0200
     8.2 +++ b/src/Tools/nbe.ML	Tue Sep 30 12:49:18 2008 +0200
     8.3 @@ -385,7 +385,7 @@
     8.4            let
     8.5              val ts' = take_until is_dict ts;
     8.6              val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
     8.7 -            val (_, T) = Code.default_typ thy c;
     8.8 +            val (_, T) = Code.default_typscheme thy c;
     8.9              val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
    8.10              val typidx' = typidx + maxidx_of_typ T' + 1;
    8.11            in of_apps bounds (Term.Const (c, T'), ts') typidx' end