# HG changeset patch
# User haftmann
# Date 1255515601 -7200
# Node ID 6bcc35f7ff6dc817429f3b80a06c630426eae452
# Parent  7a20fd22ba01575c7b0f8c1388961c34bfc567b4
more explicit notion of canonized code equations

diff -r 7a20fd22ba01 -r 6bcc35f7ff6d src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Oct 14 12:19:17 2009 +0200
+++ b/src/Pure/Isar/code.ML	Wed Oct 14 12:20:01 2009 +0200
@@ -28,6 +28,7 @@
   val const_typ_eqn: theory -> thm -> string * typ
   val typscheme_eqn: theory -> thm -> (string * sort) list * typ
   val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
+  val same_typscheme: theory -> thm list -> thm list
 
   (*executable code*)
   val add_datatype: (string * typ) list -> theory -> theory
diff -r 7a20fd22ba01 -r 6bcc35f7ff6d src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:19:17 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:20:01 2009 +0200
@@ -86,7 +86,7 @@
       * ((string * stmt) list * (string * stmt) list)) list
 
   val expand_eta: theory -> int -> thm -> thm
-  val clean_thms: theory -> thm list -> thm list
+  val canonize_thms: theory -> thm list -> thm list
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
@@ -446,9 +446,9 @@
     val var_subst = mk_desymbolization I I Var vs;
   in Thm.certify_instantiate ([], var_subst) thm end;
 
-fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
-
-fun clean_thms thy = map (Thm.transfer thy) #> same_arity thy #> desymbolize_all_vars thy;
+fun canonize_thms thy = map (Thm.transfer thy)
+  #> Code.same_typscheme thy #> desymbolize_tvars thy
+  #> same_arity thy #> map (desymbolize_vars thy);
 
 
 (** statements, abstract programs **)
@@ -614,7 +614,7 @@
       #>> (fn class => Classparam (c, class));
     fun stmt_fun raw_eqns =
       let
-        val eqns = burrow_fst (clean_thms thy) raw_eqns;
+        val eqns = burrow_fst (canonize_thms thy) raw_eqns;
         val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns);
       in
         fold_map (translate_tyvar_sort thy algbr eqngr) vs