src/HOL/HOL.thy
changeset 42477 52fa26b6c524
parent 42459 38b9f023cc34
child 42795 66fcc9882784
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 26 21:05:52 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 26 21:27:01 2011 +0200
     1.3 @@ -927,22 +927,17 @@
     1.4  done
     1.5  
     1.6  ML {*
     1.7 -structure Blast = Blast
     1.8 -(
     1.9 -  val thy = @{theory}
    1.10 -  type claset = Classical.claset
    1.11 -  val equality_name = @{const_name HOL.eq}
    1.12 -  val not_name = @{const_name Not}
    1.13 -  val notE = @{thm notE}
    1.14 -  val ccontr = @{thm ccontr}
    1.15 -  val contr_tac = Classical.contr_tac
    1.16 -  val dup_intr = Classical.dup_intr
    1.17 -  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.18 -  val rep_cs = Classical.rep_cs
    1.19 -  val cla_modifiers = Classical.cla_modifiers
    1.20 -  val cla_meth' = Classical.cla_meth'
    1.21 -);
    1.22 -val blast_tac = Blast.blast_tac;
    1.23 +  structure Blast = Blast
    1.24 +  (
    1.25 +    structure Classical = Classical
    1.26 +    val thy = @{theory}
    1.27 +    val equality_name = @{const_name HOL.eq}
    1.28 +    val not_name = @{const_name Not}
    1.29 +    val notE = @{thm notE}
    1.30 +    val ccontr = @{thm ccontr}
    1.31 +    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.32 +  );
    1.33 +  val blast_tac = Blast.blast_tac;
    1.34  *}
    1.35  
    1.36  setup Blast.setup