# HG changeset patch
# User blanchet
# Date 1284474818 -7200
# Node ID 9cab71c20613c6725e70a1e0ee17f073afb44d65
# Parent  61f0d36840c5fb28eecfa8c6e4ee7d2decea55f0
remove more clutter related to old "fast_descrs" optimization

diff -r 61f0d36840c5 -r 9cab71c20613 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Sep 14 15:39:57 2010 +0200
+++ b/src/HOL/Nitpick.thy	Tue Sep 14 16:33:38 2010 +0200
@@ -30,13 +30,10 @@
 
 axiomatization unknown :: 'a
            and is_unknown :: "'a \<Rightarrow> bool"
-           and undefined_fast_The :: 'a
-           and undefined_fast_Eps :: 'a
            and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
            and bisim_iterator_max :: bisim_iterator
            and Quot :: "'a \<Rightarrow> 'b"
            and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
-           and safe_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
 datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
 datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
@@ -95,10 +92,10 @@
                 else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
 
 definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
-"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
+"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
 
 definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
-"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
+"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
 
 inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
 "fold_graph' f z {} z" |
@@ -239,12 +236,11 @@
 
 setup {* Nitpick_Isar.setup *}
 
-hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
-    bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
-    wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
-    int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
-    norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
-    less_frac less_eq_frac of_frac
+hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
+    FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
+    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
+    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
+    number_of_frac inverse_frac less_frac less_eq_frac of_frac
 hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
     word
 hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def