src/Pure/Isar/skip_proof.ML
changeset 15801 d2f5ca3c048d
parent 15667 b7bdc1651198
child 15831 aa58e4ec3a1f
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Apr 21 22:00:28 2005 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 21 22:02:06 2005 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4      (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
     1.5    val global_skip_proof:
     1.6      bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
     1.7 -  val setup: (theory -> theory) list
     1.8  end;
     1.9  
    1.10  structure SkipProof: SKIP_PROOF =
    1.11 @@ -38,8 +37,8 @@
    1.12    if ! quick_and_dirty then t
    1.13    else error "Proof may be skipped in quick_and_dirty mode only!";
    1.14  
    1.15 -val setup =
    1.16 -  [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
    1.17 +val _ = Context.add_setup
    1.18 + [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
    1.19  
    1.20  
    1.21  (* basic cheating *)