# HG changeset patch
# User haftmann
# Date 1242027639 -7200
# Node ID 11001968caaeba23bca26f914cafc6886a7ec1c4
# Parent  36a011423fccb04e06d4793e854b9d34defb46aa
tuned interface of module Code_Unit

diff -r 36a011423fcc -r 11001968caae src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Mon May 11 09:40:38 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML	Mon May 11 09:40:39 2009 +0200
@@ -38,9 +38,9 @@
   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_eqn: theory -> thm -> string
   val const_typ_eqn: thm -> string * typ
-  val head_eqn: theory -> thm -> string * ((string * sort) list * 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
@@ -390,18 +390,19 @@
   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)
+  | 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);
 
+val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
 
-fun mk_eqn thy = add_linear o assert_eqn thy o AxClass.unoverload thy
-  o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+fun typscheme_eqn thy = typscheme thy o const_typ_eqn;
 
-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;
+(*permissive wrt. to overloaded constants!*)
+fun mk_eqn thy = add_linear o assert_eqn thy o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn;
 
 
 (* case cerificates *)
diff -r 36a011423fcc -r 11001968caae src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Mon May 11 09:40:38 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Mon May 11 09:40:39 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;