# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257914086 -3600
# Node ID 0b24a016f6dd3c2f0817a6ba14dca99fc388f270
# Parent  72a53b07d264d1fb73a4a36e517bd4317315b9f9
tuned

diff -r 72a53b07d264 -r 0b24a016f6dd ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Tue Nov 10 12:17:08 2009 +0100
+++ b/ProgTutorial/General.thy	Wed Nov 11 05:34:46 2009 +0100
@@ -1013,18 +1013,18 @@
   the latter @{ML_ind unify in Pattern} both implemented in the structure
   @{ML_struct Pattern}. An example for higher-order pattern unification is
 
-  \ldots
-*}
-
-ML{*let
-  val pat = @{term_pat "?X"}
-  val trm = @{term "a"}
-  val init = (Vartab.empty, Vartab.empty)
+  @{ML_response_fake [display, gray]
+  "let
+  val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
+  val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
+  val init = Envir.empty 0
+  val env = Pattern.unify @{theory} (trm1, trm2) init
 in
-  Pattern.match @{theory} (pat, trm) init
-end *}
-
-text {*
+  pretty_env @{context} (Envir.term_env env)
+end"
+  "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
+
+
   An assumption of this function is that the terms to be unified have 
   already the same type. In case of failure, the exceptions that are raised
   are either @{text Pattern}, @{text MATCH} or @{text Unif}.
diff -r 72a53b07d264 -r 0b24a016f6dd ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Tue Nov 10 12:17:08 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Nov 11 05:34:46 2009 +0100
@@ -2482,7 +2482,8 @@
   \end{exercise}
 
   \begin{readmore}
-  See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. 
+  See @{ML_file "Pure/conv.ML"} and  @{ML_file "Tools/more_conv.ML"}
+  for more information about conversion combinators. 
   Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
   \end{readmore}
diff -r 72a53b07d264 -r 0b24a016f6dd progtutorial.pdf
Binary file progtutorial.pdf has changed