# HG changeset patch
# User haftmann
# Date 1241441386 -7200
# Node ID cbec39ebf8f21281c25fdf851ad996822c4f7d84
# Parent  5ee6368d622bdbc6ee577e0c33625667ee774886
class typerep inherits from type

diff -r 5ee6368d622b -r cbec39ebf8f2 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Thu Apr 30 14:46:59 2009 -0700
+++ b/src/HOL/Code_Eval.thy	Mon May 04 14:49:46 2009 +0200
@@ -23,7 +23,7 @@
 code_datatype Const App
 
 class term_of = typerep +
-  fixes term_of :: "'a::{} \<Rightarrow> term"
+  fixes term_of :: "'a \<Rightarrow> term"
 
 lemma term_of_anything: "term_of x \<equiv> t"
   by (rule eq_reflection) (cases "term_of x", cases t, simp)
@@ -67,18 +67,19 @@
       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
       |> LocalTheory.exit_global
     end;
-  fun interpretator (tyco, (raw_vs, _)) thy =
-    let
-      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
-      val constrain_sort =
-        curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
-      val vs = (map o apsnd) constrain_sort raw_vs;
-      val ty = Type (tyco, map TFree vs);
-    in
-      thy
-      |> Typerep.perhaps_add_def tyco
-      |> not has_inst ? add_term_of_def ty vs tyco
-    end;
+  fun interpretator ("prop", (raw_vs, _)) thy = thy
+    | interpretator (tyco, (raw_vs, _)) thy =
+        let
+          val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+          val constrain_sort =
+            curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
+          val vs = (map o apsnd) constrain_sort raw_vs;
+          val ty = Type (tyco, map TFree vs);
+        in
+          thy
+          |> Typerep.perhaps_add_def tyco
+          |> not has_inst ? add_term_of_def ty vs tyco
+        end;
 in
   Code.type_interpretation interpretator
 end
@@ -105,21 +106,22 @@
       thy
       |> Code.add_eqn thm
     end;
-  fun interpretator (tyco, (raw_vs, raw_cs)) thy =
-    let
-      val constrain_sort =
-        curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
-      val vs = (map o apsnd) constrain_sort raw_vs;
-      val cs = (map o apsnd o map o map_atyps)
-        (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
-      val ty = Type (tyco, map TFree vs);
-      val eqs = map (mk_term_of_eq ty vs tyco) cs;
-      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
-    in
-      thy
-      |> Code.del_eqns const
-      |> fold (prove_term_of_eq ty) eqs
-    end;
+  fun interpretator ("prop", (raw_vs, _)) thy = thy
+    | interpretator (tyco, (raw_vs, raw_cs)) thy =
+        let
+          val constrain_sort =
+            curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
+          val vs = (map o apsnd) constrain_sort raw_vs;
+          val cs = (map o apsnd o map o map_atyps)
+            (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
+          val ty = Type (tyco, map TFree vs);
+          val eqs = map (mk_term_of_eq ty vs tyco) cs;
+          val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+        in
+          thy
+          |> Code.del_eqns const
+          |> fold (prove_term_of_eq ty) eqs
+        end;
 in
   Code.type_interpretation interpretator
 end
@@ -146,13 +148,13 @@
   by (subst term_of_anything) rule 
 
 code_type "term"
-  (SML "Term.term")
+  (Eval "Term.term")
 
 code_const Const and App
-  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")
+  (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
 
 code_const "term_of \<Colon> message_string \<Rightarrow> term"
-  (SML "Message'_String.mk")
+  (Eval "Message'_String.mk")
 
 
 subsection {* Evaluation setup *}
diff -r 5ee6368d622b -r cbec39ebf8f2 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Thu Apr 30 14:46:59 2009 -0700
+++ b/src/HOL/Typerep.thy	Mon May 04 14:49:46 2009 +0200
@@ -11,7 +11,7 @@
 datatype typerep = Typerep message_string "typerep list"
 
 class typerep =
-  fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
+  fixes typerep :: "'a itself \<Rightarrow> typerep"
 begin
 
 definition typerep_of :: "'a \<Rightarrow> typerep" where
@@ -79,8 +79,7 @@
 *}
 
 setup {*
-  Typerep.add_def @{type_name prop}
-  #> Typerep.add_def @{type_name fun}
+  Typerep.add_def @{type_name fun}
   #> Typerep.add_def @{type_name itself}
   #> Typerep.add_def @{type_name bool}
   #> TypedefPackage.interpretation Typerep.perhaps_add_def
@@ -92,12 +91,12 @@
   by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
 
 code_type typerep
-  (SML "Term.typ")
+  (Eval "Term.typ")
 
 code_const Typerep
-  (SML "Term.Type/ (_, _)")
+  (Eval "Term.Type/ (_, _)")
 
-code_reserved SML Term
+code_reserved Eval Term
 
 hide (open) const typerep Typerep