src/Pure/subgoal.ML
changeset 58950 d07464875dd4
parent 54883 dd04a8b654fc
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/subgoal.ML	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/Pure/subgoal.ML	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4        |> Thm.adjust_maxidx_thm idx
     1.5        |> singleton (Variable.export ctxt2 ctxt0);
     1.6    in
     1.7 -    Thm.bicompose {flatten = true, match = false, incremented = false}
     1.8 +    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
     1.9        (false, result, Thm.nprems_of st1) i st0
    1.10    end;
    1.11