# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274977826 -7200
# Node ID 31f1ec832d39ba3134eea335d9c27b1549ab5a5d
# Parent  0c1dcdefb51581ea2898ea8fc3e517350e238bf0
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set

diff -r 0c1dcdefb515 -r 31f1ec832d39 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu May 27 18:30:26 2010 +0200
@@ -383,7 +383,7 @@
 
 declare [[trace_eqvt = false]]
 
-text {* Problem: there is no raw eqvt-rule for The *}
+text {* there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
 apply(perm_strict_simp exclude: The)
 apply(perm_simp exclude: The)
diff -r 0c1dcdefb515 -r 31f1ec832d39 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Thu May 27 18:30:26 2010 +0200
@@ -47,13 +47,13 @@
   val merge = Item_Net.merge);
 
 structure EqvtRawData = Generic_Data
-( type T = thm Symtab.table;
-  val empty = Symtab.empty;
+( type T = thm Termtab.table;
+  val empty = Termtab.empty;
   val extend = I;
-  val merge = Symtab.merge (K true));
+  val merge = Termtab.merge (K true));
 
 val eqvts = Item_Net.content o EqvtData.get;
-val eqvts_raw = map snd o Symtab.dest o EqvtRawData.get;
+val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get;
 
 val get_eqvts_thms = eqvts o  Context.Proof;
 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
@@ -63,17 +63,17 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.update (c, thm))
+    Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) 
   | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 
 
 fun del_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.delete c)
+    Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c)
   | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 
 
 fun is_eqvt ctxt trm =
   case trm of 
-    Const (c, _) => Symtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
+    (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
   | _ => raise TERM ("Term must be a constsnt.", [trm])
 
 
diff -r 0c1dcdefb515 -r 31f1ec832d39 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Thu May 27 18:30:26 2010 +0200
@@ -29,8 +29,6 @@
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
 
 
-
-
 end
 
 
diff -r 0c1dcdefb515 -r 31f1ec832d39 Nominal/NewAlpha.thy
--- a/Nominal/NewAlpha.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal/NewAlpha.thy	Thu May 27 18:30:26 2010 +0200
@@ -206,7 +206,7 @@
 
   val (alphas, lthy') = Inductive.add_inductive_i
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
-      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+      coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
      all_alpha_names [] all_alpha_eqs [] lthy
 
   val alpha_ts_loc = #preds alphas;