1.1 --- a/src/HOL/Code_Eval.thy	Thu Apr 30 14:46:59 2009 -0700
     1.2 +++ b/src/HOL/Code_Eval.thy	Mon May 04 14:49:46 2009 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  code_datatype Const App
     1.5  
     1.6  class term_of = typerep +
     1.7 -  fixes term_of :: "'a::{} \<Rightarrow> term"
     1.8 +  fixes term_of :: "'a \<Rightarrow> term"
     1.9  
    1.10  lemma term_of_anything: "term_of x \<equiv> t"
    1.11    by (rule eq_reflection) (cases "term_of x", cases t, simp)
    1.12 @@ -67,18 +67,19 @@
    1.13        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.14        |> LocalTheory.exit_global
    1.15      end;
    1.16 -  fun interpretator (tyco, (raw_vs, _)) thy =
    1.17 -    let
    1.18 -      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    1.19 -      val constrain_sort =
    1.20 -        curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    1.21 -      val vs = (map o apsnd) constrain_sort raw_vs;
    1.22 -      val ty = Type (tyco, map TFree vs);
    1.23 -    in
    1.24 -      thy
    1.25 -      |> Typerep.perhaps_add_def tyco
    1.26 -      |> not has_inst ? add_term_of_def ty vs tyco
    1.27 -    end;
    1.28 +  fun interpretator ("prop", (raw_vs, _)) thy = thy
    1.29 +    | interpretator (tyco, (raw_vs, _)) thy =
    1.30 +        let
    1.31 +          val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    1.32 +          val constrain_sort =
    1.33 +            curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    1.34 +          val vs = (map o apsnd) constrain_sort raw_vs;
    1.35 +          val ty = Type (tyco, map TFree vs);
    1.36 +        in
    1.37 +          thy
    1.38 +          |> Typerep.perhaps_add_def tyco
    1.39 +          |> not has_inst ? add_term_of_def ty vs tyco
    1.40 +        end;
    1.41  in
    1.42    Code.type_interpretation interpretator
    1.43  end
    1.44 @@ -105,21 +106,22 @@
    1.45        thy
    1.46        |> Code.add_eqn thm
    1.47      end;
    1.48 -  fun interpretator (tyco, (raw_vs, raw_cs)) thy =
    1.49 -    let
    1.50 -      val constrain_sort =
    1.51 -        curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    1.52 -      val vs = (map o apsnd) constrain_sort raw_vs;
    1.53 -      val cs = (map o apsnd o map o map_atyps)
    1.54 -        (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
    1.55 -      val ty = Type (tyco, map TFree vs);
    1.56 -      val eqs = map (mk_term_of_eq ty vs tyco) cs;
    1.57 -      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    1.58 -    in
    1.59 -      thy
    1.60 -      |> Code.del_eqns const
    1.61 -      |> fold (prove_term_of_eq ty) eqs
    1.62 -    end;
    1.63 +  fun interpretator ("prop", (raw_vs, _)) thy = thy
    1.64 +    | interpretator (tyco, (raw_vs, raw_cs)) thy =
    1.65 +        let
    1.66 +          val constrain_sort =
    1.67 +            curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    1.68 +          val vs = (map o apsnd) constrain_sort raw_vs;
    1.69 +          val cs = (map o apsnd o map o map_atyps)
    1.70 +            (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
    1.71 +          val ty = Type (tyco, map TFree vs);
    1.72 +          val eqs = map (mk_term_of_eq ty vs tyco) cs;
    1.73 +          val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    1.74 +        in
    1.75 +          thy
    1.76 +          |> Code.del_eqns const
    1.77 +          |> fold (prove_term_of_eq ty) eqs
    1.78 +        end;
    1.79  in
    1.80    Code.type_interpretation interpretator
    1.81  end
    1.82 @@ -146,13 +148,13 @@
    1.83    by (subst term_of_anything) rule 
    1.84  
    1.85  code_type "term"
    1.86 -  (SML "Term.term")
    1.87 +  (Eval "Term.term")
    1.88  
    1.89  code_const Const and App
    1.90 -  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")
    1.91 +  (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
    1.92  
    1.93  code_const "term_of \<Colon> message_string \<Rightarrow> term"
    1.94 -  (SML "Message'_String.mk")
    1.95 +  (Eval "Message'_String.mk")
    1.96  
    1.97  
    1.98  subsection {* Evaluation setup *}

     2.1 --- a/src/HOL/Typerep.thy	Thu Apr 30 14:46:59 2009 -0700
     2.2 +++ b/src/HOL/Typerep.thy	Mon May 04 14:49:46 2009 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  datatype typerep = Typerep message_string "typerep list"
     2.5  
     2.6  class typerep =
     2.7 -  fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
     2.8 +  fixes typerep :: "'a itself \<Rightarrow> typerep"
     2.9  begin
    2.10  
    2.11  definition typerep_of :: "'a \<Rightarrow> typerep" where
    2.12 @@ -79,8 +79,7 @@
    2.13  *}
    2.14  
    2.15  setup {*
    2.16 -  Typerep.add_def @{type_name prop}
    2.17 -  #> Typerep.add_def @{type_name fun}
    2.18 +  Typerep.add_def @{type_name fun}
    2.19    #> Typerep.add_def @{type_name itself}
    2.20    #> Typerep.add_def @{type_name bool}
    2.21    #> TypedefPackage.interpretation Typerep.perhaps_add_def
    2.22 @@ -92,12 +91,12 @@
    2.23    by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
    2.24  
    2.25  code_type typerep
    2.26 -  (SML "Term.typ")
    2.27 +  (Eval "Term.typ")
    2.28  
    2.29  code_const Typerep
    2.30 -  (SML "Term.Type/ (_, _)")
    2.31 +  (Eval "Term.Type/ (_, _)")
    2.32  
    2.33 -code_reserved SML Term
    2.34 +code_reserved Eval Term
    2.35  
    2.36  hide (open) const typerep Typerep
    2.37