# HG changeset patch
# User blanchet
# Date 1370838629 14400
# Node ID ebd1f691866337ce336d732c058ba96fd04998bd
# Parent  acb4f932dd24f75b07bd1f771ecf64d02b5f42bb
tuning

diff -r acb4f932dd24 -r ebd1f6918663 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sat Jun 08 19:40:19 2013 -0700
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Jun 10 00:30:29 2013 -0400
@@ -157,6 +157,7 @@
     map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
   end;
 
+val id_def = @{thm id_def};
 val mp_conj = @{thm mp_conj};
 
 val simp_attrs = @{attributes [simp]};
@@ -523,8 +524,8 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
-    val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
+    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
+    val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs;
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
@@ -676,10 +677,10 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
+    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
     val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
-    val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
+    val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;