src/Pure/Isar/expression.ML
changeset 30777 9960ff945c52
parent 30776 fcd49e932503
child 30778 46de352e018b
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:47:58 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 18:06:14 2009 +0200
     1.3 @@ -416,7 +416,7 @@
     1.4         prep true false ([], []) I raw_elems raw_concl context;
     1.5       val (_, context') = context |>
     1.6         ProofContext.set_stmt true |>
     1.7 -       activate elems;
     1.8 +       fold_map activate elems;
     1.9    in (concl, context') end;
    1.10  
    1.11  in
    1.12 @@ -444,7 +444,7 @@
    1.13        fold (Context.proof_map o Locale.activate_facts) deps;
    1.14      val (elems', _) = context' |>
    1.15        ProofContext.set_stmt true |>
    1.16 -      activate elems;
    1.17 +      fold_map activate elems;
    1.18    in ((fixed, deps, elems'), (parms, ctxt')) end;
    1.19  
    1.20  in