src/Pure/raw_simplifier.ML
changeset 58950 d07464875dd4
parent 58859 d5ff8b782b29
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/raw_simplifier.ML	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -1306,7 +1306,7 @@
     1.4      val _ =
     1.5        cond_tracing ctxt (fn () =>
     1.6          print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct));
     1.7 -  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
     1.8 +  in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
     1.9  
    1.10  val simple_prover =
    1.11    SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));