--- a/Nominal/Ex/Datatypes.thy	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/Ex/Datatypes.thy	Mon Nov 07 13:58:18 2011 +0000
@@ -8,7 +8,6 @@
   atom_decl - example by John Matthews
 *)
 
-
 nominal_datatype 'a Maybe = 
   Nothing 
 | Just 'a

--- a/Nominal/Ex/Lambda.thy	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Mon Nov 07 13:58:18 2011 +0000
@@ -12,21 +12,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
-ML {* Method.SIMPLE_METHOD' *}
-ML {* Sign.intern_const *}
-
-ML {*
-val test:((Proof.context -> Method.method) context_parser) =
-Scan.succeed (fn ctxt =>
- let
-   val _ = Inductive.the_inductive ctxt "local.frees_lst_graph"
- in 
-   Method.SIMPLE_METHOD' (K (all_tac))
- end)
-*}
-
-method_setup test = {* test *} {* test *}
-
 section {* Simple examples from Norrish 2004 *}
 
 nominal_primrec 

--- a/Nominal/ROOT.ML	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/ROOT.ML	Mon Nov 07 13:58:18 2011 +0000
@@ -5,7 +5,7 @@
     "Eqvt",
     "Ex/Weakening",
     "Ex/Classical",
-    (*"Ex/Datatypes",*)
+    "Ex/Datatypes",
     "Ex/Ex1",
     "Ex/ExPS3",
     "Ex/Multi_Recs",
@@ -22,7 +22,7 @@
     "Ex/Shallow",
     "Ex/SystemFOmega",
     "Ex/TypeSchemes",
-    (*"Ex/TypeVarsTest",*)
+    "Ex/TypeVarsTest",
     "Ex/Foo1",
     "Ex/Foo2",
     "Ex/CoreHaskell",

--- a/Nominal/nominal_dt_quot.ML	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Nov 07 13:58:18 2011 +0000
@@ -85,7 +85,7 @@
   
     val (qs, lthy2) = define_qconsts qtys perm_specs lthy1
 
-    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws (Local_Theory.target_of lthy2)
+    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2
 
     val lifted_perm_laws = 
       map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'

--- a/Nominal/nominal_induct.ML	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/nominal_induct.ML	Mon Nov 07 13:58:18 2011 +0000
@@ -75,7 +75,7 @@
         val ys =
           if p < n then []
           else map (tune o #1) (take (p - n) ps) @ xs;
-      in Logic.list_rename_params (ys, prem) end;
+      in Logic.list_rename_params ys prem end;
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;