diff -r 89158f401b07 -r e5d9b6bca88c Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jun 04 09:39:23 2013 +0100
@@ -418,10 +418,6 @@
 
     val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy'
 
-    val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
-
-    (* XXX *)
-
     (* defining the auxiliary graph *)
     fun mk_cases (MutualPart {i', fvar as (n, T), ...}) =
       let
@@ -446,6 +442,8 @@
     val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = 
       Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy''
 
+    val mutual_cont = mk_partial_rules_mutual lthy''' cont mutual'
+
     (* proof of equivalence between graph and auxiliary graph *)
     val x = Var(("x", 0), ST)
     val y = Var(("y", 1), RST)