made new countable tactic work with sorts other than 'type'

--- 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:

--- 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;