# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308085780 -3600
# Node ID 886a7c614ceda411b6fab68a592a176dca35be5f
# Parent  21b5d0145fe4d64e204aaabab443e55585353d5c
updated to new Isabelle

diff -r 21b5d0145fe4 -r 886a7c614ced ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue May 17 19:46:53 2011 +0200
+++ b/ProgTutorial/Essential.thy	Tue Jun 14 22:09:40 2011 +0100
@@ -1124,13 +1124,14 @@
   as an introduction rule. Applying it directly can lead to unexpected
   behaviour since the unification has more than one solution. One way round
   this problem is to instantiate the schematic variables @{text "?P"} and
-  @{text "?x"}.  instantiation function for theorems is @{ML_ind instantiate
-  in Drule} from the structure @{ML_struct Drule}. One problem, however, is
+  @{text "?x"}.  instantiation function for theorems is 
+  @{ML_ind instantiate_normalize in Drule} from the structure 
+  @{ML_struct Drule}. One problem, however, is
   that this function expects the instantiations as lists of @{ML_type ctyp}
   and @{ML_type cterm} pairs:
 
   \begin{isabelle}
-  @{ML instantiate in Drule}@{text ":"}
+  @{ML instantiate_normalize in Drule}@{text ":"}
   @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
   \end{isabelle}
 
@@ -1183,7 +1184,7 @@
   val trm = @{term \"Trueprop (Q True)\"}
   val inst = matcher_inst @{theory} pat trm 1
 in
-  Drule.instantiate inst @{thm spec}
+  Drule.instantiate_normalize inst @{thm spec}
 end"
   "\<forall>x. Q x \<Longrightarrow> Q True"}
 
diff -r 21b5d0145fe4 -r 886a7c614ced ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Tue May 17 19:46:53 2011 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Jun 14 22:09:40 2011 +0100
@@ -876,7 +876,7 @@
   @{thm [source] rule}. For this the function @{ML_ind first_order_match in Thm} 
   matches two @{ML_type cterm}s and produces, in the successful case, a matcher 
   that can be used to instantiate the theorem. The instantiation 
-  can be done with the function @{ML_ind instantiate in Drule}. To automate 
+  can be done with the function @{ML_ind instantiate_normalize in Drule}. To automate 
   this we implement the following function.
 *}
 
@@ -885,7 +885,7 @@
     val concl_pat = Drule.strip_imp_concl (cprop_of thm)
     val insts = Thm.first_order_match (concl_pat, concl)
   in
-    rtac (Drule.instantiate insts thm) 1
+    rtac (Drule.instantiate_normalize insts thm) 1
   end)*}
 
 text {*
diff -r 21b5d0145fe4 -r 886a7c614ced progtutorial.pdf
Binary file progtutorial.pdf has changed