diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Higman.thy	Sun Aug 24 14:42:24 2008 +0200
@@ -339,6 +339,17 @@
 
 subsection {* Some examples *}
 
+instantiation LT and TT :: default
+begin
+
+definition "default = L0 [] []"
+
+definition "default = T0 A [] [] [] R0"
+
+instance ..
+
+end
+
 (* an attempt to express examples in HOL -- function
   mk_word :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
 where
@@ -354,16 +365,12 @@
 by pat_completeness auto
 termination by (relation "measure ((op -) 1001)") auto
 
-fun
+primrec
   mk_word' :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
 where
   "mk_word' 0 = mk_word 0"
   | "mk_word' (Suc n) = (do _ \<leftarrow> mk_word 0; mk_word' n done)"*)
 
-consts_code
-  "arbitrary :: LT"  ("({* L0 [] [] *})")
-  "arbitrary :: TT"  ("({* T0 A [] [] [] R0 *})")
-
 code_module Higman
 contains
   higman = higman_idx
@@ -415,17 +422,6 @@
 end;
 *}
 
-definition
-  arbitrary_LT :: LT where
-  [symmetric, code inline]: "arbitrary_LT = arbitrary"
-
-definition
-  arbitrary_TT :: TT where
-  [symmetric, code inline]: "arbitrary_TT = arbitrary"
-
-code_datatype L0 L1 arbitrary_LT
-code_datatype T0 T1 T2 arbitrary_TT
-
 ML {*
 val a = 16807.0;
 val m = 2147483647.0;