diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Prolog/Test.thy	Tue Oct 06 15:14:28 2015 +0200
@@ -80,7 +80,7 @@
 
 lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
 
-schematic_lemma "append ?x ?y [a,b,c,d]"
+schematic_goal "append ?x ?y [a,b,c,d]"
   apply (prolog prog_Test)
   back
   back
@@ -88,56 +88,56 @@
   back
   done
 
-schematic_lemma "append [a,b] y ?L"
+schematic_goal "append [a,b] y ?L"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "!y. append [a,b] y (?L y)"
+schematic_goal "!y. append [a,b] y (?L y)"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "reverse [] ?L"
+schematic_goal "reverse [] ?L"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "reverse [23] ?L"
+schematic_goal "reverse [23] ?L"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "reverse [23,24,?x] ?L"
+schematic_goal "reverse [23,24,?x] ?L"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "reverse ?L [23,24,?x]"
+schematic_goal "reverse ?L [23,24,?x]"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "mappred age ?x [23,24]"
+schematic_goal "mappred age ?x [23,24]"
   apply (prolog prog_Test)
   back
   done
 
-schematic_lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
+schematic_goal "mappred (%x y. ? z. age z y) ?x [23,24]"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "mappred ?P [bob,sue] [24,23]"
+schematic_goal "mappred ?P [bob,sue] [24,23]"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
+schematic_goal "mapfun f [bob,bob,sue] [?x,?y,?z]"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "mapfun (%x. h x 25) [bob,sue] ?L"
+schematic_goal "mapfun (%x. h x 25) [bob,sue] ?L"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
+schematic_goal "mapfun ?F [24,25] [h bob 24,h bob 25]"
   apply (prolog prog_Test)
   done
 
-schematic_lemma "mapfun ?F [24] [h 24 24]"
+schematic_goal "mapfun ?F [24] [h 24 24]"
   apply (prolog prog_Test)
   back
   back
@@ -148,12 +148,12 @@
   apply (prolog prog_Test)
   done
 
-schematic_lemma "age ?x 24 & age ?y 23"
+schematic_goal "age ?x 24 & age ?y 23"
   apply (prolog prog_Test)
   back
   done
 
-schematic_lemma "age ?x 24 | age ?x 23"
+schematic_goal "age ?x 24 | age ?x 23"
   apply (prolog prog_Test)
   back
   back
@@ -167,7 +167,7 @@
   apply (prolog prog_Test)
   done
 
-schematic_lemma "age sue 24 .. age bob 23 => age ?x ?y"
+schematic_goal "age sue 24 .. age bob 23 => age ?x ?y"
   apply (prolog prog_Test)
   back
   back
@@ -181,7 +181,7 @@
   done
 (*reset trace_DEPTH_FIRST;*)
 
-schematic_lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
+schematic_goal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
   apply (prolog prog_Test)
   back
   back
@@ -192,7 +192,7 @@
   apply (prolog prog_Test)
   done
 
-schematic_lemma "? P. P & eq P ?x"
+schematic_goal "? P. P & eq P ?x"
   apply (prolog prog_Test)
 (*
   back
@@ -247,14 +247,14 @@
   by fast
 *)
 
-schematic_lemma "!Emp Stk.(
+schematic_goal "!Emp Stk.(
                        empty    (Emp::'b) .. 
          (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
          (!(X::nat) S. remove X ((Stk X S)::'b) S))
  => bag_appl 23 24 ?X ?Y"
   oops
 
-schematic_lemma "!Qu. ( 
+schematic_goal "!Qu. ( 
           (!L.            empty    (Qu L L)) .. 
           (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
           (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
@@ -265,7 +265,7 @@
   apply (prolog prog_Test)
   done
 
-schematic_lemma "P x .. P y => P ?X"
+schematic_goal "P x .. P y => P ?X"
   apply (prolog prog_Test)
   back
   done