# HG changeset patch
# User haftmann
# Date 1255521416 -7200
# Node ID 0e9e13ac06d770f8d4c4b7c574024380376883ed
# Parent  6bcc35f7ff6dc817429f3b80a06c630426eae452
sharpened name

diff -r 6bcc35f7ff6d -r 0e9e13ac06d7 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Oct 14 12:20:01 2009 +0200
+++ b/src/Pure/Isar/code.ML	Wed Oct 14 13:56:56 2009 +0200
@@ -28,7 +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
+  val standard_typscheme: theory -> thm list -> thm list
 
   (*executable code*)
   val add_datatype: (string * typ) list -> theory -> theory
@@ -532,7 +532,7 @@
         ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
   in map (cert o assert_eqn thy) eqns end;
 
-fun same_typscheme thy thms =
+fun standard_typscheme thy thms =
   let
     fun tvars_of T = rev (Term.add_tvarsT T []);
     val vss = map (tvars_of o snd o head_eqn) thms;
@@ -546,7 +546,7 @@
 fun these_eqns thy c =
   get_eqns thy c
   |> (map o apfst) (Thm.transfer thy)
-  |> burrow_fst (same_typscheme thy);
+  |> burrow_fst (standard_typscheme thy);
 
 fun all_eqns thy =
   Symtab.dest ((the_eqns o the_exec) thy)
diff -r 6bcc35f7ff6d -r 0e9e13ac06d7 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:20:01 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Oct 14 13:56:56 2009 +0200
@@ -447,7 +447,7 @@
   in Thm.certify_instantiate ([], var_subst) thm end;
 
 fun canonize_thms thy = map (Thm.transfer thy)
-  #> Code.same_typscheme thy #> desymbolize_tvars thy
+  #> Code.standard_typscheme thy #> desymbolize_tvars thy
   #> same_arity thy #> map (desymbolize_vars thy);