1.1 --- a/src/Pure/Isar/code.ML	Wed Oct 14 12:20:01 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Oct 14 13:56:56 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    val const_typ_eqn: theory -> thm -> string * typ
     1.5    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
     1.6    val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
     1.7 -  val same_typscheme: theory -> thm list -> thm list
     1.8 +  val standard_typscheme: theory -> thm list -> thm list
     1.9  
    1.10    (*executable code*)
    1.11    val add_datatype: (string * typ) list -> theory -> theory
    1.12 @@ -532,7 +532,7 @@
    1.13          ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
    1.14    in map (cert o assert_eqn thy) eqns end;
    1.15  
    1.16 -fun same_typscheme thy thms =
    1.17 +fun standard_typscheme thy thms =
    1.18    let
    1.19      fun tvars_of T = rev (Term.add_tvarsT T []);
    1.20      val vss = map (tvars_of o snd o head_eqn) thms;
    1.21 @@ -546,7 +546,7 @@
    1.22  fun these_eqns thy c =
    1.23    get_eqns thy c
    1.24    |> (map o apfst) (Thm.transfer thy)
    1.25 -  |> burrow_fst (same_typscheme thy);
    1.26 +  |> burrow_fst (standard_typscheme thy);
    1.27  
    1.28  fun all_eqns thy =
    1.29    Symtab.dest ((the_eqns o the_exec) thy)

     2.1 --- a/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:20:01 2009 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Oct 14 13:56:56 2009 +0200
     2.3 @@ -447,7 +447,7 @@
     2.4    in Thm.certify_instantiate ([], var_subst) thm end;
     2.5  
     2.6  fun canonize_thms thy = map (Thm.transfer thy)
     2.7 -  #> Code.same_typscheme thy #> desymbolize_tvars thy
     2.8 +  #> Code.standard_typscheme thy #> desymbolize_tvars thy
     2.9    #> same_arity thy #> map (desymbolize_vars thy);
    2.10  
    2.11