src/Sequents/simpdata.ML
changeset 17481 75166ebb619b
parent 12725 7ede865e1fe5
child 17876 b9c92f384109
     1.1 --- a/src/Sequents/simpdata.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/simpdata.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  fun prove_fun s =
     1.6   (writeln s;
     1.7 -  prove_goal LK.thy s
     1.8 +  prove_goal (the_context ()) s
     1.9     (fn prems => [ (cut_facts_tac prems 1),
    1.10                    (fast_tac (pack() add_safes [subst]) 1) ]));
    1.11  
    1.12 @@ -144,7 +144,7 @@
    1.13  
    1.14  (*** Named rewrite rules ***)
    1.15  
    1.16 -fun prove nm thm  = qed_goal nm LK.thy thm
    1.17 +fun prove nm thm  = qed_goal nm (the_context ()) thm
    1.18      (fn prems => [ (cut_facts_tac prems 1),
    1.19                     (fast_tac LK_pack 1) ]);
    1.20  
    1.21 @@ -264,7 +264,7 @@
    1.22  
    1.23  (* To create substition rules *)
    1.24  
    1.25 -qed_goal "eq_imp_subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
    1.26 +qed_goal "eq_imp_subst" (the_context ()) "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
    1.27    (fn prems =>
    1.28     [cut_facts_tac prems 1,
    1.29      asm_simp_tac LK_basic_ss 1]);