--- a/Nominal/nominal_dt_rawperm.ML	Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML	Mon Aug 16 17:39:16 2010 +0800
@@ -9,8 +9,8 @@
 
 signature NOMINAL_DT_RAWPERM =
 sig
-  val define_raw_perms: string list -> typ list -> term list -> thm -> theory -> 
-    (term list * thm list * thm list) * theory
+  val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory -> 
+    (term list * thm list * thm list) * local_theory
 end
 
 
@@ -20,7 +20,7 @@
 
 (** proves the two pt-type class properties **)
 
-fun prove_permute_zero lthy induct perm_defs perm_fns =
+fun prove_permute_zero induct perm_defs perm_fns lthy =
 let
   val perm_types = map (body_type o fastype_of) perm_fns
   val perm_indnames = Datatype_Prop.make_tnames perm_types
@@ -42,7 +42,7 @@
 end
 
 
-fun prove_permute_plus lthy induct perm_defs perm_fns =
+fun prove_permute_plus induct perm_defs perm_fns lthy =
 let
   val p = Free ("p", @{typ perm})
   val q = Free ("q", @{typ perm})
@@ -90,7 +90,7 @@
 end
 
 
-fun define_raw_perms full_ty_names tys constrs induct_thm thy =
+fun define_raw_perms full_ty_names tys constrs induct_thm lthy =
 let
   val perm_fn_names = full_ty_names
     |> map Long_Name.base_name
@@ -102,15 +102,6 @@
 
   val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
 
-  val lthy =
-    Class.instantiation (full_ty_names, [], @{sort pt}) thy
-   
-  val ((perm_funs, perm_eq_thms), lthy') =
-    Primrec.add_primrec perm_fn_binds perm_eqs lthy;
-    
-  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
-  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
-  
   fun tac _ (_, _, simps) =
     Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
   
@@ -118,10 +109,20 @@
     (map (Morphism.term phi) fvs, 
      map (Morphism.thm phi) dfs, 
      map (Morphism.thm phi) simps);
+
+  val ((perm_funs, perm_eq_thms), lthy') =
+    lthy
+    |> Local_Theory.exit_global
+    |> Class.instantiation (full_ty_names, [], @{sort pt}) 
+    |> Primrec.add_primrec perm_fn_binds perm_eqs
+    
+  val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
+  val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' 
 in
   lthy'
   |> Class.prove_instantiation_exit_result morphism tac 
        (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
+  ||> Named_Target.theory_init
 end