src/HOL/Induct/Term.thy

--- a/src/HOL/Induct/Term.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Induct/Term.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -42,9 +42,9 @@
 text {* \medskip Alternative induction rule *}
 
 lemma
-  (assumes var: "!!v. P (Var v)"
-    and app: "!!f ts. list_all P ts ==> P (App f ts)")
-  term_induct2: "P t"
+  assumes var: "!!v. P (Var v)"
+    and app: "!!f ts. list_all P ts ==> P (App f ts)"
+  shows term_induct2: "P t"
 and "list_all P ts"
   apply (induct t and ts)
      apply (rule var)