--- a/Nominal/NewParser.thy	Thu Jul 15 09:40:05 2010 +0100
+++ b/Nominal/NewParser.thy	Fri Jul 16 02:38:19 2010 +0100
@@ -359,7 +359,8 @@
   val (alpha_distincts, alpha_bn_distincts) = 
     mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
 
-  (* definition of raw_alpha_eq_iff  lemmas *)
+  (* definition of alpha_eq_iff  lemmas *)
+  (* they have a funny shape for the simplifier *)
   val _ = warning "Eq-iff theorems";
   val alpha_eq_iff = 
     if get_STEPS lthy > 5
@@ -470,10 +471,18 @@
   (* respectfulness proofs *)
   
   (* HERE *)
+
+  val (_, lthy8') = lthy8
+     |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
+     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) 
+     ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
+     ||>> Local_Theory.note ((@{binding "perm_defs"}, []), raw_perm_defs) 
+     ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
+
   
   val _ = 
     if get_STEPS lthy > 16
-    then true else raise TEST lthy8
+    then true else raise TEST lthy8'
   
   (* old stuff *)