--- 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
--- 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")
--- 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
--- 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")
--- 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,
--- 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];