# HG changeset patch
# User blanchet
# Date 1410186146 -7200
# Node ID 7b70a2b4ec9b7ec91b0e9b6a386ce6d5c97c24aa
# Parent  ad45b22a0b3935f1c55dca5904d5ea0a07ba4399
made new countable tactic work with sorts other than 'type'

diff -r ad45b22a0b39 -r 7b70a2b4ec9b src/HOL/BNF_Examples/Misc_Datatype.thy
--- a/src/HOL/BNF_Examples/Misc_Datatype.thy	Mon Sep 08 16:14:21 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Mon Sep 08 16:22:26 2014 +0200
@@ -183,7 +183,7 @@
 instance mylist :: (countable) countable
   by countable_datatype
 
-instance some_passive :: (countable, countable , countable, countable) countable
+instance some_passive :: (countable, "{countable,ord}", countable, countable) countable
   by countable_datatype
 
 (* TODO: Enable once "fset" is registered as countable:
diff -r ad45b22a0b39 -r 7b70a2b4ec9b src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Mon Sep 08 16:14:21 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Mon Sep 08 16:22:26 2014 +0200
@@ -134,7 +134,8 @@
           SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
         | _ => not_datatype s);
 
-      val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
+      val fpTs0 as Type (_, var_As) :: _ =
+        map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
       val fpT_names = map (fst o dest_Type) fpTs0;
 
       val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;