--- a/Nominal/nominal_dt_quot.ML	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Wed Aug 25 09:02:06 2010 +0800
@@ -13,11 +13,11 @@
   val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
     Quotient_Info.qconsts_info list * local_theory
 
-  val define_qperms: typ list -> string list -> (string * term * mixfix) list -> 
-    thm list -> local_theory -> local_theory
+  val define_qperms: typ list -> string list -> (string * sort) list -> 
+    (string * term * mixfix) list -> thm list -> local_theory -> local_theory
 
-  val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> 
-    local_theory -> local_theory
+  val define_qsizes: typ list -> string list -> (string * sort) list -> 
+    (string * term * mixfix) list -> local_theory -> local_theory
 
   val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm
 end
@@ -47,46 +47,62 @@
 
 
 (* defines the quotient permutations and proves pt-class *)
-fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws lthy =
+fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
 let
-  val lthy' = 
+  val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys))
+
+  val lthy1 = 
     lthy
     |> Local_Theory.exit_global
-    |> Class.instantiation (qfull_ty_names, [], @{sort pt}) 
+    |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
   
-  val (_, lthy'') = define_qconsts qtys perm_specs lthy'
+  val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
+
+  val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
 
-  val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys []) raw_perm_laws
+  val lifted_perm_laws = 
+    map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
+    |> Variable.exportT lthy3 lthy2
 
   fun tac _ =
     Class.intro_classes_tac [] THEN
       (ALLGOALS (resolve_tac lifted_perm_laws))
 in
-  lthy''
+  lthy2
   |> Class.prove_instantiation_exit tac 
   |> Named_Target.theory_init
 end
 
 
 (* defines the size functions and proves size-class *)
-fun define_qsizes qtys qfull_ty_names size_specs lthy =
+fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
 let
   fun tac _ = Class.intro_classes_tac []
 in
   lthy
   |> Local_Theory.exit_global
-  |> Class.instantiation (qfull_ty_names, [], @{sort size})
+  |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
   |> snd o (define_qconsts qtys size_specs)
   |> Class.prove_instantiation_exit tac
   |> Named_Target.theory_init
 end
 
 
-(* lifts a theorem and deletes all "_raw" suffixes *)
+(* lifts a theorem and cleans all "_raw" instances 
+   from variable names *)
 
-fun unraw_str s = 
-  unsuffix "_raw" s
-  handle Fail _ => s
+local
+  val any = Scan.one (Symbol.not_eof)
+  val raw = Scan.this_string "_raw"
+  val exclude =
+    Scan.repeat (Scan.unless raw any) --| raw >> implode
+  val parser = Scan.repeat (exclude || any)
+in
+  fun unraw_str s =
+   s |> explode
+     |> Scan.finite Symbol.stopper parser >> implode 
+     |> fst
+end
 
 fun unraw_vars_thm thm =
 let
@@ -111,6 +127,7 @@
   |> Quotient_Tacs.lifted ctxt qtys simps
   |> unraw_bounds_thm
   |> unraw_vars_thm
+  |> Drule.zero_var_indexes
 
 
 end (* structure *)