# HG changeset patch
# User blanchet
# Date 1383646662 -3600
# Node ID 3e1d230f1c0067dc1a18b89b4eb595b18e096189
# Parent  27501a51d847012dde0c2a73145c9668d08ab716
make local theory operations non-pervasive (makes more intuitive sense)

diff -r 27501a51d847 -r 3e1d230f1c00 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Nov 05 09:45:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Nov 05 11:17:42 2013 +0100
@@ -1313,7 +1313,7 @@
   end;
 
 fun register_bnf key (bnf, lthy) =
-  (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
+  (bnf, Local_Theory.declaration {syntax = false, pervasive = false}
     (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy);
 
 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
diff -r 27501a51d847 -r 3e1d230f1c00 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 05 09:45:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 05 11:17:42 2013 +0100
@@ -179,7 +179,7 @@
 (* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *)
 
 fun register_fp_sugar key fp_sugar =
-  Local_Theory.declaration {syntax = false, pervasive = true}
+  Local_Theory.declaration {syntax = false, pervasive = false}
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
diff -r 27501a51d847 -r 3e1d230f1c00 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 09:45:03 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 11:17:42 2013 +0100
@@ -78,15 +78,13 @@
   | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t)
   | unfold_let t = t;
 
-val dummy_var_name = "?f"
-
 fun mk_map_pattern ctxt s =
   let
     val bnf = the (bnf_of ctxt s);
     val mapx = map_of_bnf bnf;
     val live = live_of_bnf bnf;
     val (f_Ts, _) = strip_typeN live (fastype_of mapx);
-    val fs = map_index (fn (i, T) => Var ((dummy_var_name, i), T)) f_Ts;
+    val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts;
   in
     (mapx, betapplys (mapx, fs))
   end;
diff -r 27501a51d847 -r 3e1d230f1c00 src/HOL/BNF/Tools/ctr_sugar.ML
--- a/src/HOL/BNF/Tools/ctr_sugar.ML	Tue Nov 05 09:45:03 2013 +0100
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Tue Nov 05 11:17:42 2013 +0100
@@ -139,7 +139,7 @@
   Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
 
 fun register_ctr_sugar key ctr_sugar =
-  Local_Theory.declaration {syntax = false, pervasive = true}
+  Local_Theory.declaration {syntax = false, pervasive = false}
     (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
 
 val rep_compat_prefix = "new";
@@ -918,7 +918,7 @@
         (ctr_sugar,
          lthy
          |> not rep_compat ?
-            (Local_Theory.declaration {syntax = false, pervasive = true}
+            (Local_Theory.declaration {syntax = false, pervasive = false}
                (fn phi => Case_Translation.register
                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
          |> Local_Theory.notes (anonymous_notes @ notes) |> snd