1.1 --- a/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:00 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:25 2008 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4  ML
     1.5  {*
     1.6  val analz_mono_contra_tac = 
     1.7 -  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
     1.8 +  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
     1.9    in
    1.10      rtac analz_impI THEN' 
    1.11      REPEAT1 o 
    1.12 @@ -334,7 +334,7 @@
    1.13  
    1.14  
    1.15  val synth_analz_mono_contra_tac = 
    1.16 -  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.17 +  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.18    in
    1.19      rtac syan_impI THEN' 
    1.20      REPEAT1 o 

     2.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 18:02:00 2008 +0200
     2.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Wed Jun 11 18:02:25 2008 +0200
     2.3 @@ -789,7 +789,7 @@
     2.4      be pulled out using the @{text analz_insert} rules*}
     2.5  ML
     2.6  {*
     2.7 -fun insComm x y = inst "x" x (inst "y" y insert_commute);
     2.8 +fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
     2.9  
    2.10  bind_thms ("pushKeys",
    2.11             map (insComm "Key ?K") 

     3.1 --- a/src/HOL/Auth/Event.thy	Wed Jun 11 18:02:00 2008 +0200
     3.2 +++ b/src/HOL/Auth/Event.thy	Wed Jun 11 18:02:25 2008 +0200
     3.3 @@ -281,7 +281,7 @@
     3.4  ML
     3.5  {*
     3.6  val analz_mono_contra_tac = 
     3.7 -  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
     3.8 +  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
     3.9    in
    3.10      rtac analz_impI THEN' 
    3.11      REPEAT1 o 
    3.12 @@ -299,7 +299,7 @@
    3.13  ML
    3.14  {*
    3.15  val synth_analz_mono_contra_tac = 
    3.16 -  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    3.17 +  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    3.18    in
    3.19      rtac syan_impI THEN' 
    3.20      REPEAT1 o 

     4.1 --- a/src/HOL/Auth/Message.thy	Wed Jun 11 18:02:00 2008 +0200
     4.2 +++ b/src/HOL/Auth/Message.thy	Wed Jun 11 18:02:25 2008 +0200
     4.3 @@ -821,7 +821,7 @@
     4.4      be pulled out using the @{text analz_insert} rules*}
     4.5  ML
     4.6  {*
     4.7 -fun insComm x y = inst "x" x (inst "y" y insert_commute);
     4.8 +fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
     4.9  
    4.10  bind_thms ("pushKeys",
    4.11             map (insComm "Key ?K") 

     5.1 --- a/src/HOL/Real/rat_arith.ML	Wed Jun 11 18:02:00 2008 +0200
     5.2 +++ b/src/HOL/Real/rat_arith.ML	Wed Jun 11 18:02:25 2008 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4  val simprocs = field_cancel_numeral_factors
     5.5  
     5.6  val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
     5.7 -             inst "a" "(number_of ?v)" @{thm right_distrib},
     5.8 +             OldGoals.inst "a" "(number_of ?v)" @{thm right_distrib},
     5.9               @{thm divide_1}, @{thm divide_zero_left},
    5.10               @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    5.11               @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,

     6.1 --- a/src/ZF/int_arith.ML	Wed Jun 11 18:02:00 2008 +0200
     6.2 +++ b/src/ZF/int_arith.ML	Wed Jun 11 18:02:25 2008 +0200
     6.3 @@ -11,16 +11,16 @@
     6.4      such as -x = #3
     6.5  **)
     6.6  
     6.7 -Addsimps [inst "y" "integ_of(?w)" @{thm zminus_equation},
     6.8 -          inst "x" "integ_of(?w)" @{thm equation_zminus}];
     6.9 +Addsimps [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_equation},
    6.10 +          OldGoals.inst "x" "integ_of(?w)" @{thm equation_zminus}];
    6.11  
    6.12 -AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zless},
    6.13 -         inst "x" "integ_of(?w)" @{thm zless_zminus}];
    6.14 +AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zless},
    6.15 +         OldGoals.inst "x" "integ_of(?w)" @{thm zless_zminus}];
    6.16  
    6.17 -AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zle},
    6.18 -         inst "x" "integ_of(?w)" @{thm zle_zminus}];
    6.19 +AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zle},
    6.20 +         OldGoals.inst "x" "integ_of(?w)" @{thm zle_zminus}];
    6.21  
    6.22 -Addsimps [inst "s" "integ_of(?w)" @{thm Let_def}];
    6.23 +Addsimps [OldGoals.inst "s" "integ_of(?w)" @{thm Let_def}];
    6.24  
    6.25  (*** Simprocs for numeric literals ***)
    6.26  
    6.27 @@ -48,10 +48,10 @@
    6.28  
    6.29  (** For cancel_numerals **)
    6.30  
    6.31 -val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
    6.32 +val rel_iff_rel_0_rls = map (OldGoals.inst "y" "?u$+?v")
    6.33                            [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    6.34                             zle_iff_zdiff_zle_0] @
    6.35 -                        map (inst "y" "n")
    6.36 +                        map (OldGoals.inst "y" "n")
    6.37                            [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    6.38                             zle_iff_zdiff_zle_0];
    6.39