# HG changeset patch
# User urbanc
# Date 1130885669 -3600
# Node ID 004515accc10754eb152413e9701acd9a6f3c6df
# Parent  dba086ed50cb4d1d7d3b7383f8a241c79b8cfc45
tunings of some comments (nothing serious)

diff -r dba086ed50cb -r 004515accc10 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon Oct 31 16:35:15 2005 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue Nov 01 23:54:29 2005 +0100
@@ -9,21 +9,24 @@
 (*      tuple_lambda [a] t       produces %a . t                              *) 
 (*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)
 
-  fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
-    | tuple_lambda [x] t = lambda x t
-    | tuple_lambda (x::xs) t =
-       let
-         val t' = tuple_lambda xs t;
-         val Type ("fun", [T,U]) = fastype_of t';
-       in
-         HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
-       end; 
+fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
+  | tuple_lambda [x] t = lambda x t
+  | tuple_lambda (x::xs) t =
+    let
+        val t' = tuple_lambda xs t;
+        val Type ("fun", [T,U]) = fastype_of t';
+    in
+        HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
+    end; 
 
 fun find_var frees name =
   (case Library.find_first (equal name o fst o dest_Free) frees of
     NONE => error ("No such Variable in term: " ^ quote name)
   | SOME v => v);
 
+(* - names specifies the variables that are involved in the *)
+(*   induction                                              *)
+(* - rule is the induction rule to be applied               *)              
 fun nominal_induct_tac (names, rule) facts state =
   let
     val sg     = Thm.sign_of_thm state;
@@ -38,7 +41,7 @@
         val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
         val (P :: ts, x) = split_last concl_vars
           handle Empty => error "Malformed conclusion of induction rule"
-            | Bind => error "Malformed conclusion of induction rule";
+               | Bind  => error "Malformed conclusion of induction rule";
       in
         cterm_instantiate
           ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
diff -r dba086ed50cb -r 004515accc10 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Mon Oct 31 16:35:15 2005 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Nov 01 23:54:29 2005 +0100
@@ -103,11 +103,6 @@
 
 in             
 
-(* FIXME simp_modifiers' 
-
-(Markus needs to commit this)
-*)
-
 
 fun simp_meth_setup tac =
   Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)