src/HOL/Code_Evaluation.thy

--- a/src/HOL/Code_Evaluation.thy	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy	Mon Feb 22 11:10:20 2010 +0100
@@ -76,7 +76,8 @@
         andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
     in if need_inst then add_term_of tyco raw_vs thy else thy end;
 in
-  Code.type_interpretation ensure_term_of
+  Code.datatype_interpretation ensure_term_of
+  #> Code.abstype_interpretation ensure_term_of
 end
 *}
 
@@ -114,7 +115,7 @@
       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
     in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
 in
-  Code.type_interpretation ensure_term_of_code
+  Code.datatype_interpretation ensure_term_of_code
 end
 *}