# HG changeset patch
# User wenzelm
# Date 1213200145 -7200
# Node ID 026f3db3f5c6262328bc2d77e92b615ac4f26f52
# Parent  56b6cdce22f1b6f136002fc764e96d167e4e319e
OldGoals.inst;

diff -r 56b6cdce22f1 -r 026f3db3f5c6 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -261,7 +261,7 @@
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   in
     rtac analz_impI THEN' 
     REPEAT1 o 
@@ -334,7 +334,7 @@
 
 
 val synth_analz_mono_contra_tac = 
-  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
+  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   in
     rtac syan_impI THEN' 
     REPEAT1 o 
diff -r 56b6cdce22f1 -r 026f3db3f5c6 doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -789,7 +789,7 @@
     be pulled out using the @{text analz_insert} rules*}
 ML
 {*
-fun insComm x y = inst "x" x (inst "y" y insert_commute);
+fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
 
 bind_thms ("pushKeys",
            map (insComm "Key ?K") 
diff -r 56b6cdce22f1 -r 026f3db3f5c6 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/src/HOL/Auth/Event.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -281,7 +281,7 @@
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   in
     rtac analz_impI THEN' 
     REPEAT1 o 
@@ -299,7 +299,7 @@
 ML
 {*
 val synth_analz_mono_contra_tac = 
-  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
+  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   in
     rtac syan_impI THEN' 
     REPEAT1 o 
diff -r 56b6cdce22f1 -r 026f3db3f5c6 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -821,7 +821,7 @@
     be pulled out using the @{text analz_insert} rules*}
 ML
 {*
-fun insComm x y = inst "x" x (inst "y" y insert_commute);
+fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
 
 bind_thms ("pushKeys",
            map (insComm "Key ?K") 
diff -r 56b6cdce22f1 -r 026f3db3f5c6 src/HOL/Real/rat_arith.ML
--- a/src/HOL/Real/rat_arith.ML	Wed Jun 11 18:02:00 2008 +0200
+++ b/src/HOL/Real/rat_arith.ML	Wed Jun 11 18:02:25 2008 +0200
@@ -13,7 +13,7 @@
 val simprocs = field_cancel_numeral_factors
 
 val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
-             inst "a" "(number_of ?v)" @{thm right_distrib},
+             OldGoals.inst "a" "(number_of ?v)" @{thm right_distrib},
              @{thm divide_1}, @{thm divide_zero_left},
              @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
              @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
diff -r 56b6cdce22f1 -r 026f3db3f5c6 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Wed Jun 11 18:02:00 2008 +0200
+++ b/src/ZF/int_arith.ML	Wed Jun 11 18:02:25 2008 +0200
@@ -11,16 +11,16 @@
     such as -x = #3
 **)
 
-Addsimps [inst "y" "integ_of(?w)" @{thm zminus_equation},
-          inst "x" "integ_of(?w)" @{thm equation_zminus}];
+Addsimps [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_equation},
+          OldGoals.inst "x" "integ_of(?w)" @{thm equation_zminus}];
 
-AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zless},
-         inst "x" "integ_of(?w)" @{thm zless_zminus}];
+AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zless},
+         OldGoals.inst "x" "integ_of(?w)" @{thm zless_zminus}];
 
-AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zle},
-         inst "x" "integ_of(?w)" @{thm zle_zminus}];
+AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zle},
+         OldGoals.inst "x" "integ_of(?w)" @{thm zle_zminus}];
 
-Addsimps [inst "s" "integ_of(?w)" @{thm Let_def}];
+Addsimps [OldGoals.inst "s" "integ_of(?w)" @{thm Let_def}];
 
 (*** Simprocs for numeric literals ***)
 
@@ -48,10 +48,10 @@
 
 (** For cancel_numerals **)
 
-val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
+val rel_iff_rel_0_rls = map (OldGoals.inst "y" "?u$+?v")
                           [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
                            zle_iff_zdiff_zle_0] @
-                        map (inst "y" "n")
+                        map (OldGoals.inst "y" "n")
                           [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
                            zle_iff_zdiff_zle_0];