src/Pure/Isar/skip_proof.ML
changeset 30288 a32700e45ab3
parent 29606 fedb8be05f24
child 32966 5b21661fe618
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Mar 05 18:19:20 2009 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Mar 05 19:48:02 2009 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  (* oracle setup *)
     1.5  
     1.6  val (_, skip_proof) = Context.>>> (Context.map_theory_result
     1.7 -  (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
     1.8 +  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
     1.9      if ! quick_and_dirty then Thm.cterm_of thy prop
    1.10      else error "Proof may be skipped in quick_and_dirty mode only!")));
    1.11