src/HOL/HOL.thy
changeset 51687 3d8720271ebf
parent 51314 eac4bb5adbf9
child 51689 43a3465805dd
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 10 17:02:47 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 10 17:17:16 2013 +0200
     1.3 @@ -843,11 +843,6 @@
     1.4  open Basic_Classical;
     1.5  *}
     1.6  
     1.7 -setup {*
     1.8 -  ML_Antiquote.value @{binding claset}
     1.9 -    (Scan.succeed "Classical.claset_of ML_context")
    1.10 -*}
    1.11 -
    1.12  setup Classical.setup
    1.13  
    1.14  setup {*
    1.15 @@ -888,7 +883,7 @@
    1.16  declare exE [elim!]
    1.17    allE [elim]
    1.18  
    1.19 -ML {* val HOL_cs = @{claset} *}
    1.20 +ML {* val HOL_cs = claset_of @{context} *}
    1.21  
    1.22  lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
    1.23    apply (erule swap)