src/Tools/Code/code_thingol.ML
changeset 32928 6bcc35f7ff6d
parent 32917 84a5c684a22e
child 32929 0e9e13ac06d7
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:19:17 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:20:01 2009 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4        * ((string * stmt) list * (string * stmt) list)) list
     1.5  
     1.6    val expand_eta: theory -> int -> thm -> thm
     1.7 -  val clean_thms: theory -> thm list -> thm list
     1.8 +  val canonize_thms: theory -> thm list -> thm list
     1.9    val read_const_exprs: theory -> string list -> string list * string list
    1.10    val consts_program: theory -> string list -> string list * (naming * program)
    1.11    val cached_program: theory -> naming * program
    1.12 @@ -446,9 +446,9 @@
    1.13      val var_subst = mk_desymbolization I I Var vs;
    1.14    in Thm.certify_instantiate ([], var_subst) thm end;
    1.15  
    1.16 -fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
    1.17 -
    1.18 -fun clean_thms thy = map (Thm.transfer thy) #> same_arity thy #> desymbolize_all_vars thy;
    1.19 +fun canonize_thms thy = map (Thm.transfer thy)
    1.20 +  #> Code.same_typscheme thy #> desymbolize_tvars thy
    1.21 +  #> same_arity thy #> map (desymbolize_vars thy);
    1.22  
    1.23  
    1.24  (** statements, abstract programs **)
    1.25 @@ -614,7 +614,7 @@
    1.26        #>> (fn class => Classparam (c, class));
    1.27      fun stmt_fun raw_eqns =
    1.28        let
    1.29 -        val eqns = burrow_fst (clean_thms thy) raw_eqns;
    1.30 +        val eqns = burrow_fst (canonize_thms thy) raw_eqns;
    1.31          val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns);
    1.32        in
    1.33          fold_map (translate_tyvar_sort thy algbr eqngr) vs