
diff -r 3444a24dc4e9 -r c2ca2c3d23a6 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Mar 13 23:45:34 2012 +0100
+++ b/src/HOL/Induct/Term.thy	Wed Mar 14 00:34:56 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* Terms over a given alphabet *}
 
-theory Term imports Main begin
+theory Term
+imports Main
+begin
 
 datatype ('a, 'b) "term" =
     Var 'a
@@ -14,7 +16,8 @@
 text {* \medskip Substitution function on terms *}
 
 primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
-  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
+  and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+where
   "subst_term f (Var a) = f a"
 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
 | "subst_term_list f [] = []"




