# HG changeset patch
# User blanchet
# Date 1409730180 -7200
# Node ID deeff89d5b9ec5b6c92a3da0f02d1165c015e512
# Parent  e4965b677ba980249d7d4411514d4f85402054a6
added compatibility function

diff -r e4965b677ba9 -r deeff89d5b9e src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Sep 03 00:31:38 2014 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Sep 03 09:43:00 2014 +0200
@@ -161,7 +161,7 @@
 qed
 
 ML {*
-  fun old_countable_tac ctxt =
+  fun old_countable_datatype_tac ctxt =
     SUBGOAL (fn (goal, _) =>
       let
         val ty_name =
@@ -201,10 +201,18 @@
 
 ML_file "bnf_lfp_countable.ML"
 
+ML {*
+fun countable_datatype_tac ctxt st =
+  HEADGOAL (old_countable_datatype_tac ctxt) st
+  handle ERROR _ => BNF_LFP_Countable.countable_datatype_tac ctxt st;
+
+(* compatibility *)
+fun countable_tac ctxt =
+  SELECT_GOAL (countable_datatype_tac ctxt);
+*}
+
 method_setup countable_datatype = {*
-  Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD (fn st => HEADGOAL (old_countable_tac ctxt) st
-      handle ERROR _ => BNF_LFP_Countable.countable_tac ctxt st))
+  Scan.succeed (SIMPLE_METHOD o countable_datatype_tac)
 *} "prove countable class instances for datatypes"
 
 
@@ -279,10 +287,9 @@
   show "\<exists>n. r = nat_to_rat_surj n"
   proof (cases r)
     fix i j assume [simp]: "r = Fract i j" and "j > 0"
-    have "r = (let m = int_encode i; n = int_encode j
-               in nat_to_rat_surj(prod_encode (m,n)))"
+    have "r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))"
       by (simp add: Let_def nat_to_rat_surj_def)
-    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
+    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp: Let_def)
   qed
 qed
 
diff -r e4965b677ba9 -r deeff89d5b9e src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 00:31:38 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 09:43:00 2014 +0200
@@ -7,7 +7,7 @@
 
 signature BNF_LFP_COUNTABLE =
 sig
-  val countable_tac: Proof.context -> tactic
+  val countable_datatype_tac: Proof.context -> tactic
 end;
 
 structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
@@ -30,7 +30,7 @@
     dtac meta_spec THEN' meta_spec_mp_tac (n - 1) THEN' dtac meta_mp THEN' atac;
 
 val use_induction_hypothesis_tac =
-  DEEPEN (1, 1000000 (* large number *))
+  DEEPEN (1, 64 (* large number *))
     (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0;
 
 val same_ctr_simps =
@@ -119,7 +119,7 @@
     let
       fun not_datatype s = error (quote s ^ " is not a new-style datatype");
       fun not_mutually_recursive ss =
-        error ("{" ^ commas ss ^ "} is not a set of mutually recursive new-style datatypes");
+        error ("{" ^ commas ss ^ "} are not mutually recursive new-style datatypes");
 
       fun lfp_sugar_of s =
         (case fp_sugar_of ctxt s of
@@ -162,7 +162,7 @@
     in
       Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
         mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
-        inj_map_strongs')
+          inj_map_strongs')
       |> HOLogic.conj_elims
       |> Proof_Context.export names_ctxt ctxt
       |> map Thm.close_derivation
@@ -171,13 +171,13 @@
 fun get_countable_goal_typ (@{const Trueprop} $ (Const (@{const_name Ex}, _)
     $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
         $ Const (@{const_name top}, _)))) = s
-  | get_countable_goal_typ _ = error "Wrong goal format for countable tactic";
+  | get_countable_goal_typ _ = error "Wrong goal format for datatype countability tactic";
 
-fun core_countable_tac ctxt st =
+fun core_countable_datatype_tac ctxt st =
   endgame_tac ctxt (mk_encode_injective_thms ctxt (map get_countable_goal_typ (Thm.prems_of st)))
     st;
 
-fun countable_tac ctxt =
-  TRY (Class.intro_classes_tac []) THEN core_countable_tac ctxt;
+fun countable_datatype_tac ctxt =
+  TRY (Class.intro_classes_tac []) THEN core_countable_datatype_tac ctxt;
 
 end;