src/HOL/HOL.thy
changeset 48776 37cd53e69840
parent 48195 3127f9ce52fb
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 11 21:32:46 2012 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 11 22:17:46 2012 +0200
     1.3 @@ -847,7 +847,7 @@
     1.4  
     1.5  setup {*
     1.6    ML_Antiquote.value @{binding claset}
     1.7 -    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())")
     1.8 +    (Scan.succeed "Classical.claset_of ML_context")
     1.9  *}
    1.10  
    1.11  setup Classical.setup