| changeset 32176 | 893614e2c35c |
| parent 32172 | c4e55f30d527 |
| child 32402 | 5731300da417 |
--- a/src/HOL/HOL.thy Fri Jul 24 21:18:05 2009 +0200 +++ b/src/HOL/HOL.thy Fri Jul 24 21:21:45 2009 +0200 @@ -910,8 +910,9 @@ done ML {* -structure Blast = BlastFun +structure Blast = Blast ( + val thy = @{theory} type claset = Classical.claset val equality_name = @{const_name "op ="} val not_name = @{const_name Not}