# HG changeset patch
# User blanchet
# Date 1345021495 -7200
# Node ID d1688612668dac815292af59ac74a7a857ceee71
# Parent  ef4c010c69b57975347f879f3a866bc73623eb5d
removed dead code

diff -r ef4c010c69b5 -r d1688612668d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 15 01:17:26 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 15 11:04:55 2012 +0200
@@ -754,7 +754,7 @@
     (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
        SOME (Const (s', _)) =>
        s = s' andalso not (is_registered_type ctxt abs_T)
-     | NONE => false)
+     | _ => false)
   | is_quot_rep_fun _ _ = false
 
 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
@@ -1298,14 +1298,6 @@
   is_frac_type ctxt (Type (s, []))
 fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
   | is_funky_typedef _ _ = false
-fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
-    is_typedef_axiom ctxt boring t2
-  | is_typedef_axiom ctxt boring
-        (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
-         $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
-         $ Const _ $ _)) =
-    boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s
-  | is_typedef_axiom _ _ _ = false
 
 fun all_defs_of thy subst =
   let