# HG changeset patch
# User blanchet
# Date 1457389211 -3600
# Node ID 656e9653c645f676a1688a5985d36e39d4d2a0de
# Parent  cb262f03ac122f50eddb0334f563ffc560917472
made 'size' plugin compatible with locales again (and added regression test)

diff -r cb262f03ac12 -r 656e9653c645 NEWS
--- a/NEWS	Mon Mar 07 23:20:11 2016 +0100
+++ b/NEWS	Mon Mar 07 23:20:11 2016 +0100
@@ -48,6 +48,7 @@
       rel_prod_apply ~> rel_prod_inject
       pred_prod_apply ~> pred_prod_inject
     INCOMPATIBILITY.
+  - The "size" plugin has been made compatible again with locales.
 
 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
 resemble the f.split naming convention, INCOMPATIBILITY.
diff -r cb262f03ac12 -r 656e9653c645 src/HOL/Datatype_Examples/Misc_Datatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Mon Mar 07 23:20:11 2016 +0100
@@ -57,11 +57,18 @@
   ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
 *)
 
-datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
-and 'a I2 = I21 | I22 "'a I1" "'a I2"
+locale loc =
+  fixes c :: 'a and d :: 'a
+  assumes "c \<noteq> d"
+begin
 
-datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
-and 'a forest = FNil | FCons "'a tree" "'a forest"
+datatype (discs_sels) 'b I1 = I11 'b "'b I1" | I12 'b "'b I2"
+and 'b I2 = I21 | I22 "'b I1" "'b I2"
+
+datatype (discs_sels) 'b tree = TEmpty | TNode 'b "'b forest"
+and 'b forest = FNil | FCons "'b tree" "'b forest"
+
+end
 
 datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
 and 'a branch = Branch 'a "'a tree'"
@@ -217,12 +224,6 @@
   by countable_datatype
 *)
 
-instance I1 and I2 :: (countable) countable
-  by countable_datatype
-
-instance tree and forest :: (countable) countable
-  by countable_datatype
-
 instance tree' and branch :: (countable) countable
   by countable_datatype
 
@@ -318,8 +319,6 @@
 datatype_compat simple''
 datatype_compat mylist
 datatype_compat some_passive
-datatype_compat I1 I2
-datatype_compat tree forest
 datatype_compat tree' branch
 datatype_compat bin_rose_tree
 datatype_compat exp trm factor
diff -r cb262f03ac12 -r 656e9653c645 src/HOL/Datatype_Examples/Misc_Primrec.thy
--- a/src/HOL/Datatype_Examples/Misc_Primrec.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Datatype_Examples/Misc_Primrec.thy	Mon Mar 07 23:20:11 2016 +0100
@@ -53,15 +53,18 @@
   "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
   "rename_lam f (Let SL l) = Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l)"
 
-primrec
-  sum_i1 :: "('a::{zero,plus}) I1 \<Rightarrow> 'a" and
-  sum_i2 :: "'a I2 \<Rightarrow> 'a"
+primrec (in loc)
+  sum_i1 :: "('b::{zero,plus}) I1 \<Rightarrow> 'b" and
+  sum_i2 :: "'b I2 \<Rightarrow> 'b"
 where
   "sum_i1 (I11 n i) = n + sum_i1 i" |
   "sum_i1 (I12 n i) = n + sum_i2 i" |
   "sum_i2 I21 = 0" |
   "sum_i2 (I22 i j) = sum_i1 i + sum_i2 j"
 
+context loc
+begin
+
 primrec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
   "forest_of_mylist MyNil = FNil" |
   "forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)"
@@ -90,6 +93,8 @@
   "mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" |
   "mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
 
+end
+
 primrec
   id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
   id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
diff -r cb262f03ac12 -r 656e9653c645 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Mar 07 23:20:11 2016 +0100
@@ -77,7 +77,8 @@
 val size_of_global = Symtab.lookup o Data.get o Context.Theory;
 
 fun all_overloaded_size_defs_of ctxt =
-  Symtab.fold (fn (_, (_, (overloaded_size_def, _, _))) => cons overloaded_size_def)
+  Symtab.fold (fn (_, (_, (overloaded_size_def, _, _))) =>
+      can (Logic.dest_equals o Thm.prop_of) overloaded_size_def ? cons overloaded_size_def)
     (Data.get (Context.Proof ctxt)) [];
 
 val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]};