# HG changeset patch
# User krauss
# Date 1285659260 -7200
# Node ID 06fc1a79b4bf8cd6e5ff7596d5bb4f9d07db648a
# Parent  7ead9d0f2e84414fe4251fd7e85fb27dd9bbba95
removed unnecessary reference poking (cf. f45d332a90e3)

diff -r 7ead9d0f2e84 -r 06fc1a79b4bf doc-src/Functions/Thy/Functions.thy
--- a/doc-src/Functions/Thy/Functions.thy	Tue Sep 28 09:17:33 2010 +0200
+++ b/doc-src/Functions/Thy/Functions.thy	Tue Sep 28 09:34:20 2010 +0200
@@ -580,7 +580,6 @@
 | "fib2 1 = 1"
 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
 
-(*<*)ML_val "goals_limit := 1"(*>*)
 txt {*
   This kind of matching is again justified by the proof of pattern
   completeness and compatibility. 
@@ -588,7 +587,7 @@
   either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
   (2::nat)"}:
 
-  @{subgoals[display,indent=0]}
+  @{subgoals[display,indent=0,goals_limit=1]}
 
   This is an arithmetic triviality, but unfortunately the
   @{text arith} method cannot handle this specific form of an
@@ -597,7 +596,6 @@
   existentials, which can then be solved by the arithmetic decision procedure.
   Pattern compatibility and termination are automatic as usual.
 *}
-(*<*)ML_val "goals_limit := 10"(*>*)
 apply atomize_elim
 apply arith
 apply auto