# HG changeset patch
# User wenzelm
# Date 1344803968 -7200
# Node ID 234702dc4f179642f1bff97896b35e48a0d29376
# Parent  de617c90413107ef26a58b005de2358578e17835
tuned;

diff -r de617c904131 -r 234702dc4f17 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Aug 12 21:48:58 2012 +0200
+++ b/src/Pure/ML/ml_thms.ML	Sun Aug 12 22:39:28 2012 +0200
@@ -88,7 +88,7 @@
     (fn _ => Args.context -- Args.mode "open" --
         Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
           (by |-- Method.parse -- Scan.option Method.parse)) >>
-      (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
+      (fn ((ctxt, is_open), (raw_propss, methods)) =>
         let
           val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
           val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
@@ -102,7 +102,7 @@
           val thms =
             Proof_Context.get_fact ctxt'
               (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
-        in thm_binding "lemma" (length (flat propss) = 1) thms background end))));
+        in thm_binding "lemma" (length (flat propss) = 1) thms end))));
 
 end;