diff -r a94aea0cef76 -r 800787c3210f src/HOL/ex/Quickcheck_Generators.thy --- a/src/HOL/ex/Quickcheck_Generators.thy Wed May 20 15:35:12 2009 +0200 +++ b/src/HOL/ex/Quickcheck_Generators.thy Wed May 20 15:35:13 2009 +0200 @@ -12,11 +12,11 @@ "collapse f = (do g \ f; g done)" lemma random'_if: - fixes random' :: "index \ index \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" + fixes random' :: "code_numeral \ code_numeral \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" assumes "random' 0 j = (\s. undefined)" - and "\i. random' (Suc_index i) j = rhs2 i" + and "\i. random' (Suc_code_numeral i) j = rhs2 i" shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" - by (cases i rule: index.exhaust) (insert assms, simp_all) + by (cases i rule: code_numeral.exhaust) (insert assms, simp_all) setup {* let @@ -62,7 +62,7 @@ in case mk_conss thy ty ts_rec of SOME t_rec => mk_collapse thy (term_ty ty) $ (Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $ - @{term "i\index"} $ t_rec $ t_atom) + @{term "i\code_numeral"} $ t_rec $ t_atom) | NONE => t_atom end; fun mk_random_eqs thy vs tycos = @@ -73,12 +73,12 @@ val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); val random' = Free (random'_name, - @{typ index} --> @{typ index} --> this_ty'); + @{typ code_numeral} --> @{typ code_numeral} --> this_ty'); fun atom ty = if Sign.of_sort thy (ty, @{sort random}) - then ((ty, false), random ty $ @{term "j\index"}) + then ((ty, false), random ty $ @{term "j\code_numeral"}) else raise TYP ("Will not generate random elements for type(s) " ^ quote (hd tycos)); - fun dtyp tyco = ((this_ty, true), random' $ @{term "i\index"} $ @{term "j\index"}); + fun dtyp tyco = ((this_ty, true), random' $ @{term "i\code_numeral"} $ @{term "j\code_numeral"}); fun rtyp tyco tys = raise REC ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); val rhss = DatatypePackage.construction_interpretation thy @@ -87,9 +87,9 @@ |> (map o apsnd) (List.partition fst) |> map (mk_clauses thy this_ty) val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ - (random' $ @{term "0\index"} $ @{term "j\index"}, Abs ("s", @{typ Random.seed}, + (random' $ @{term "0\code_numeral"} $ @{term "j\code_numeral"}, Abs ("s", @{typ Random.seed}, Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))), - (random' $ @{term "Suc_index i"} $ @{term "j\index"}, rhs) + (random' $ @{term "Suc_code_numeral i"} $ @{term "j\code_numeral"}, rhs) ]))) rhss; in eqss end; fun random_inst [tyco] thy = @@ -99,8 +99,8 @@ (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) - (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\index"}, - random' $ @{term "max (i\index) 1"} $ @{term "i\index"}) + (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\code_numeral"}, + random' $ @{term "max (i\code_numeral) 1"} $ @{term "i\code_numeral"}) val del_func = Attrib.internal (fn _ => Thm.declaration_attribute (fn thm => Context.mapping (Code.del_eqn thm) I)); fun add_code simps lthy =