merged
authorhaftmann
Mon, 11 May 2009 17:08:31 +0200
changeset 31093 ee45b1c733c1
parent 31086 3e69a25b90a2 (current diff)
parent 31092 27a6558e64b6 (diff)
child 31097 a09767ab684d
child 31103 9820999467a7
child 31108 0ce5f53fc65d
merged
--- a/src/HOL/Library/Efficient_Nat.thy	Mon May 11 15:05:17 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon May 11 17:08:31 2009 +0200
@@ -179,10 +179,8 @@
        else NONE
   end;
 
-fun eqn_suc_preproc thy = map fst
-  #> gen_eqn_suc_preproc
-      @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
-  #> (Option.map o map) (Code_Unit.mk_eqn thy);
+val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc
+  @{thm Suc_if_eq} I (fst o Logic.dest_equals));
 
 fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
   @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
--- a/src/HOL/Tools/recfun_codegen.ML	Mon May 11 15:05:17 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 11 17:08:31 2009 +0200
@@ -25,13 +25,13 @@
 
 fun add_thm NONE thm thy = Code.add_eqn thm thy
   | add_thm (SOME module_name) thm thy =
-      case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
-       of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
-            in thy
-              |> ModuleData.map (Symtab.update (c, module_name))
-              |> Code.add_eqn thm'
-            end
-        | NONE => Code.add_eqn thm thy;
+      let
+        val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true)
+      in
+        thy
+        |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name))
+        |> Code.add_eqn thm'
+      end;
 
 fun meta_eq_to_obj_eq thy thm =
   let
@@ -57,7 +57,6 @@
     val thms = Code.these_raw_eqns thy c'
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> expand_eta thy
-      |> map (AxClass.overload thy)
       |> map_filter (meta_eq_to_obj_eq thy)
       |> Code_Unit.norm_varnames thy
       |> map (rpair opt_name)
--- a/src/HOL/Tools/typecopy_package.ML	Mon May 11 15:05:17 2009 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Mon May 11 17:08:31 2009 +0200
@@ -150,7 +150,7 @@
                 THEN ALLGOALS (rtac @{thm refl})) def_thm)
     |-> (fn def_thm => Code.add_eqn def_thm)
     |> `(fn thy => mk_eq_refl thy)
-    |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm)
+    |-> (fn refl_thm => Code.add_nbe_eqn refl_thm)
   end;
 
 val setup =
--- a/src/Pure/Isar/code.ML	Mon May 11 15:05:17 2009 +0100
+++ b/src/Pure/Isar/code.ML	Mon May 11 17:08:31 2009 +0200
@@ -8,7 +8,7 @@
 signature CODE =
 sig
   val add_eqn: thm -> theory -> theory
-  val add_nonlinear_eqn: thm -> theory -> theory
+  val add_nbe_eqn: thm -> theory -> theory
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Attrib.src
@@ -20,6 +20,8 @@
   val add_inline: thm -> theory -> theory
   val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
   val del_functrans: string -> theory -> theory
+  val simple_functrans: (theory -> thm list -> thm list option)
+    -> theory -> (thm * bool) list -> (thm * bool) list option
   val add_datatype: (string * typ) list -> theory -> theory
   val add_datatype_cmd: string list -> theory -> theory
   val type_interpretation:
@@ -109,7 +111,7 @@
 (* code equations *)
 
 type eqns = bool * (thm * bool) list lazy;
-  (*default flag, theorems with linear flag (perhaps lazy)*)
+  (*default flag, theorems with proper flag (perhaps lazy)*)
 
 fun pretty_lthms ctxt r = case Lazy.peek r
  of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
@@ -122,18 +124,18 @@
         val thy_ref = Theory.check_thy thy;
       in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
 
-fun add_drop_redundant thy (thm, linear) thms =
+fun add_drop_redundant thy (thm, proper) thms =
   let
     val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
     val args = args_of thm;
     val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
     fun matches_args args' = length args <= length args' andalso
       Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
-    fun drop (thm', linear') = if (linear orelse not linear')
+    fun drop (thm', proper') = if (proper orelse not proper')
       andalso matches_args (args_of thm') then 
         (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
       else false;
-  in (thm, linear) :: filter_out drop thms end;
+  in (thm, proper) :: filter_out drop thms end;
 
 fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
   | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
@@ -456,16 +458,6 @@
           cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
       in map (Thm.instantiate (instT, [])) thms' end;
 
-fun check_linear (eqn as (thm, linear)) =
-  if linear then eqn else Code_Unit.bad_thm
-    ("Duplicate variables on left hand side of code equation:\n"
-      ^ Display.string_of_thm thm);
-
-fun mk_eqn thy linear =
-  Code_Unit.error_thm ((if linear then check_linear else I) o Code_Unit.mk_eqn thy);
-fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy);
-fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy);
-
 
 (** interfaces and attributes **)
 
@@ -487,51 +479,47 @@
        then SOME tyco else NONE
     | _ => NONE;
 
-fun recheck_eqn thy = Code_Unit.error_thm
-  (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
+fun is_constr thy = is_some o get_datatype_of_constr thy;
+
+fun assert_eqn thy = Code_Unit.assert_eqn thy (is_constr thy);
 
-fun recheck_eqns_const thy c eqns =
+fun assert_eqns_const thy c eqns =
   let
-    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
+    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm
       then eqn else error ("Wrong head of code equation,\nexpected constant "
         ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
-  in map (cert o recheck_eqn thy) eqns end;
+  in map (cert o assert_eqn thy) eqns end;
 
 fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
   o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
     o apfst) (fn (_, eqns) => (true, f eqns));
 
-fun gen_add_eqn linear default thm thy =
-  case (if default then mk_default_eqn thy else SOME o mk_eqn thy linear) thm
-   of SOME (thm, _) =>
-        let
-          val c = Code_Unit.const_eqn thm;
-          val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
-            then error ("Rejected polymorphic code equation for overloaded constant:\n"
-              ^ Display.string_of_thm thm)
-            else ();
-          val _ = if not default andalso (is_some o get_datatype_of_constr thy) c
-            then error ("Rejected code equation for datatype constructor:\n"
-              ^ Display.string_of_thm thm)
-            else ();
-        in change_eqns false c (add_thm thy default (thm, linear)) thy end
+fun gen_add_eqn default (eqn as (thm, _)) thy =
+  let val c = Code_Unit.const_eqn thy thm
+  in change_eqns false c (add_thm thy default eqn) thy end;
+
+fun add_eqn thm thy =
+  gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, true)) thy;
+
+fun add_default_eqn thm thy =
+  case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
+   of SOME eqn => gen_add_eqn true eqn thy
     | NONE => thy;
 
-val add_eqn = gen_add_eqn true false;
-val add_default_eqn = gen_add_eqn true true;
-val add_nonlinear_eqn = gen_add_eqn false false;
+fun add_nbe_eqn thm thy =
+  gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, false)) thy;
 
 fun add_eqnl (c, lthms) thy =
   let
-    val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms;
+    val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms;
   in change_eqns false c (add_lthms lthms') thy end;
 
 val add_default_eqn_attribute = Thm.declaration_attribute
   (fn thm => Context.mapping (add_default_eqn thm) I);
 val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
 
-fun del_eqn thm thy = case mk_syntactic_eqn thy thm
- of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thm) (del_thm thm) thy
+fun del_eqn thm thy = case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm
+ of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy
   | NONE => thy;
 
 fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
@@ -553,9 +541,9 @@
           then insert (op =) c else I) cases []) cases;
   in
     thy
+    |> fold (del_eqns o fst) cs
     |> map_exec_purge NONE
         ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
-        #> map_eqns (fold (Symtab.delete_safe o fst) cs)
         #> (map_cases o apfst) drop_outdated_cases)
     |> TypeInterpretation.data (tyco, serial ())
   end;
@@ -571,7 +559,7 @@
 fun add_case thm thy =
   let
     val (c, (k, case_pats)) = Code_Unit.case_cert thm;
-    val _ = case filter (is_none o get_datatype_of_constr thy) case_pats
+    val _ = case filter_out (is_constr thy) case_pats
      of [] => ()
       | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
     val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
@@ -596,6 +584,10 @@
   (map_exec_purge NONE o map_thmproc o apsnd)
     (delete_force "function transformer" name);
 
+fun simple_functrans f thy eqns = case f thy (map fst eqns)
+ of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
+  | NONE => NONE;
+
 val _ = Context.>> (Context.map_theory
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
@@ -607,7 +599,7 @@
   in
     TypeInterpretation.init
     #> add_del_attribute ("", (add_eqn, del_eqn))
-    #> add_simple_attribute ("nbe", add_nonlinear_eqn)
+    #> add_simple_attribute ("nbe", add_nbe_eqn)
     #> add_del_attribute ("inline", (add_inline, del_inline))
     #> add_del_attribute ("post", (add_post, del_post))
   end));
@@ -621,9 +613,7 @@
   | apply_functrans thy c [] eqns = eqns
   | apply_functrans thy c functrans eqns = eqns
       |> perhaps (perhaps_loop (perhaps_apply functrans))
-      |> (map o apfst) (AxClass.unoverload thy)
-      |> recheck_eqns_const thy c
-      |> (map o apfst) (AxClass.overload thy);
+      |> assert_eqns_const thy c;
 
 fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
 
@@ -634,16 +624,17 @@
   #> Logic.dest_equals
   #> snd;
 
-fun preprocess thy functrans c eqns =
+fun preprocess thy c eqns =
   let
     val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
+    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
+      o the_thmproc o the_exec) thy;
   in
     eqns
-    |> (map o apfst) (AxClass.overload thy)
     |> apply_functrans thy c functrans
     |> (map o apfst) (Code_Unit.rewrite_eqn pre)
     |> (map o apfst) (AxClass.unoverload thy)
-    |> map (recheck_eqn thy)
+    |> map (assert_eqn thy)
     |> burrow_fst (common_typ_eqns thy)
   end;
 
@@ -677,14 +668,9 @@
   |> burrow_fst (common_typ_eqns thy);
 
 fun these_eqns thy c =
-  let
-    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
-      o the_thmproc o the_exec) thy;
-  in
-    get_eqns thy c
-    |> (map o apfst) (Thm.transfer thy)
-    |> preprocess thy functrans c
-  end;
+  get_eqns thy c
+  |> (map o apfst) (Thm.transfer thy)
+  |> preprocess thy c;
 
 fun default_typscheme thy c =
   let
@@ -693,10 +679,10 @@
     fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
   in case AxClass.class_of_param thy c
    of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c))
-    | NONE => if is_some (get_datatype_of_constr thy c)
+    | NONE => if is_constr thy c
         then strip_sorts (the_const_typscheme c)
         else case get_eqns thy c
-         of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
+         of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm
           | [] => strip_sorts (the_const_typscheme c) end;
 
 end; (*local*)
--- a/src/Pure/Isar/code_unit.ML	Mon May 11 15:05:17 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML	Mon May 11 17:08:31 2009 +0200
@@ -6,12 +6,6 @@
 
 signature CODE_UNIT =
 sig
-  (*generic non-sense*)
-  val bad_thm: string -> 'a
-  val error_thm: ('a -> 'b) -> 'a -> 'b
-  val warning_thm: ('a -> 'b) -> 'a -> 'b option
-  val try_thm: ('a -> 'b) -> 'a -> 'b option
-
   (*typ instantiations*)
   val typscheme: theory -> string * typ -> (string * sort) list * typ
   val inst_thm: theory -> sort Vartab.table -> thm -> thm
@@ -35,12 +29,12 @@
     -> string * ((string * sort) list * (string * typ list) list)
 
   (*code equations*)
-  val assert_eqn: theory -> thm -> thm
-  val mk_eqn: theory -> thm -> thm * bool
-  val assert_linear: (string -> bool) -> thm * bool -> thm * bool
-  val const_eqn: thm -> string
-  val const_typ_eqn: thm -> string * typ
-  val head_eqn: theory -> thm -> string * ((string * sort) list * typ)
+  val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
+  val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
+  val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
+  val const_eqn: theory -> thm -> string
+    val const_typ_eqn: thm -> string * typ
+  val typscheme_eqn: theory -> thm -> (string * sort) list * typ
   val expand_eta: theory -> int -> thm -> thm
   val rewrite_eqn: simpset -> thm -> thm
   val rewrite_head: thm list -> thm -> thm
@@ -57,13 +51,6 @@
 
 (* auxiliary *)
 
-exception BAD_THM of string;
-fun bad_thm msg = raise BAD_THM msg;
-fun error_thm f thm = f thm handle BAD_THM msg => error msg;
-fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
-  => (warning ("code generator: " ^ msg); NONE);
-fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
-
 fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
 fun string_of_const thy c = case AxClass.inst_of_param thy c
  of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
@@ -323,85 +310,96 @@
 
 (* code equations *)
 
-fun assert_eqn thy thm =
+exception BAD_THM of string;
+fun bad_thm msg = raise BAD_THM msg;
+fun error_thm f thm = f thm handle BAD_THM msg => error msg;
+fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
+
+fun is_linear thm =
+  let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm
+  in not (has_duplicates (op =) ((fold o fold_aterms)
+    (fn Var (v, _) => cons v | _ => I) args [])) end;
+
+fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) =
   let
     val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
       handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
-          | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
+           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
     fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
-      | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
+      | Free _ => bad_thm ("Illegal free variable in equation\n"
           ^ Display.string_of_thm thm)
       | _ => I) t [];
     fun tvars_of t = fold_term_types (fn _ =>
       fold_atyps (fn TVar (v, _) => insert (op =) v
         | TFree _ => bad_thm 
-      ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
+      ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
     val lhs_vs = vars_of lhs;
     val rhs_vs = vars_of rhs;
     val lhs_tvs = tvars_of lhs;
     val rhs_tvs = tvars_of rhs;
     val _ = if null (subtract (op =) lhs_vs rhs_vs)
       then ()
-      else bad_thm ("Free variables on right hand side of rewrite theorem\n"
+      else bad_thm ("Free variables on right hand side of equation\n"
         ^ Display.string_of_thm thm);
     val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
       then ()
-      else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
+      else bad_thm ("Free type variables on right hand side of equation\n"
         ^ Display.string_of_thm thm)    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
-    val (c, ty) = case head of Const c_ty => c_ty | _ =>
-      bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
+    val (c, ty) = case head
+     of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
+      | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
     fun check _ (Abs _) = bad_thm
           ("Abstraction on left hand side of equation\n"
             ^ Display.string_of_thm thm)
       | check 0 (Var _) = ()
       | check _ (Var _) = bad_thm
-          ("Variable with application on left hand side of code equation\n"
+          ("Variable with application on left hand side of equation\n"
             ^ Display.string_of_thm thm)
       | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
-      | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
-          then bad_thm
-            ("Partially applied constant on left hand side of equation\n"
-               ^ Display.string_of_thm thm)
-          else ();
+      | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
+          then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
+            then ()
+            else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
+              ^ Display.string_of_thm thm)
+          else bad_thm
+            ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
+               ^ Display.string_of_thm thm);
     val _ = map (check 0) args;
+    val _ = if not proper orelse is_linear thm then ()
+      else bad_thm ("Duplicate variables on left hand side of equation\n"
+        ^ Display.string_of_thm thm);
+    val _ = if (is_none o AxClass.class_of_param thy) c
+      then ()
+      else bad_thm ("Polymorphic constant as head in equation\n"
+        ^ Display.string_of_thm thm)
+    val _ = if not (is_constr_head c)
+      then ()
+      else bad_thm ("Constructor as head in equation\n"
+        ^ Display.string_of_thm thm)
     val ty_decl = Sign.the_const_type thy c;
     val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
       then () else bad_thm ("Type\n" ^ string_of_typ thy ty
-           ^ "\nof code equation\n"
+           ^ "\nof equation\n"
            ^ Display.string_of_thm thm
            ^ "\nis incompatible with declared function type\n"
            ^ string_of_typ thy ty_decl)
-  in thm end;
-
-fun add_linear thm =
-  let
-    val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
-    val linear = not (has_duplicates (op =)
-      ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
-  in (thm, linear) end;
+  in (thm, proper) end;
 
-fun assert_pat is_cons thm =
-  let
-    val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
-    val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t
-          else bad_thm ("Not a constructor on left hand side of equation: "
-            ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm)
-      | t => t) args;
-  in thm end;
-
-fun assert_linear is_cons (thm, false) = (thm, false)
-  | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true)
-      else bad_thm
-        ("Duplicate variables on left hand side of code equation:\n"
-          ^ Display.string_of_thm thm);
-
-
-fun mk_eqn thy = add_linear o assert_eqn thy o AxClass.unoverload thy
-  o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr);
 
 val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
-val const_eqn = fst o const_typ_eqn;
-fun head_eqn thy thm = let val (c, ty) = const_typ_eqn thm in (c, typscheme thy (c, ty)) end;
+
+fun typscheme_eqn thy = typscheme thy o const_typ_eqn;
+
+(*these are permissive wrt. to overloaded constants!*)
+fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
+  apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
+
+fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
+  o try_thm (gen_assert_eqn thy is_constr_head (K true))
+  o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+
+fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn;
 
 
 (* case cerificates *)
--- a/src/Tools/code/code_thingol.ML	Mon May 11 15:05:17 2009 +0100
+++ b/src/Tools/code/code_thingol.ML	Mon May 11 17:08:31 2009 +0200
@@ -591,14 +591,14 @@
             translate_term thy algbr funcgr thm t'
             ##>> fold_map (translate_term thy algbr funcgr thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and translate_eq thy algbr funcgr (thm, linear) =
+and translate_eq thy algbr funcgr (thm, proper) =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
       o Logic.unvarify o prop_of) thm;
   in
     fold_map (translate_term thy algbr funcgr (SOME thm)) args
     ##>> translate_term thy algbr funcgr (SOME thm) rhs
-    #>> rpair (thm, linear)
+    #>> rpair (thm, proper)
   end
 and translate_const thy algbr funcgr thm (c, ty) =
   let
--- a/src/Tools/code/code_wellsorted.ML	Mon May 11 15:05:17 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Mon May 11 17:08:31 2009 +0200
@@ -64,7 +64,7 @@
 fun tyscm_rhss_of thy c eqns =
   let
     val tyscm = case eqns of [] => Code.default_typscheme thy c
-      | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
+      | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm;
     val rhss = consts_of thy eqns;
   in (tyscm, rhss) end;