--- a/Nominal/Perm.thy	Tue Apr 20 09:02:22 2010 +0200
+++ b/Nominal/Perm.thy	Tue Apr 20 09:13:52 2010 +0200
@@ -2,18 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms"
 begin
 
-ML {*
-fun quotient_lift_consts_export qtys spec ctxt =
-let
-  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
-  val (ts_loc, defs_loc) = split_list result;
-  val morphism = ProofContext.export_morphism ctxt' ctxt;
-  val ts = map (Morphism.term morphism) ts_loc
-  val defs = Morphism.fact morphism defs_loc
-in
-  (ts, defs, ctxt')
-end
-*}
+
 
 ML {*
 fun prove_perm_zero lthy induct perm_def perm_frees =
@@ -132,21 +121,25 @@
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_zero_thms = List.take (prove_perm_zero lthy' induct perm_ldef perm_frees, dt_nos);
-  val perm_plus_thms = List.take (prove_perm_plus lthy' induct perm_ldef perm_frees, dt_nos)
+  val perm_zero_thms = prove_perm_zero lthy' induct perm_ldef perm_frees
+  val perm_plus_thms = prove_perm_plus lthy' induct perm_ldef perm_frees
+  val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
+  val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
   val perms_name = space_implode "_" perm_fn_names
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")
+  
   fun tac _ (_, simps, _) =
-    (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));
+    (Class.intro_classes_tac []) THEN ALLGOALS (resolve_tac simps);
+  
   fun morphism phi (dfs, simps, fvs) =
     (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
   in
     lthy'
-    |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms))
-    |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms))
+    |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
+    |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
     |> Class_Target.prove_instantiation_exit_result morphism tac 
-         (perm_ldef, (perm_zero_thms @ perm_plus_thms), perm_frees)
+         (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_frees)
   end
 *}
 
@@ -175,6 +168,19 @@
 *)
 
 ML {*
+fun quotient_lift_consts_export qtys spec ctxt =
+let
+  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
+  val (ts_loc, defs_loc) = split_list result;
+  val morphism = ProofContext.export_morphism ctxt' ctxt;
+  val ts = map (Morphism.term morphism) ts_loc
+  val defs = Morphism.fact morphism defs_loc
+in
+  (ts, defs, ctxt')
+end
+*}
+
+ML {*
 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
 let
   val lthy =