src/Pure/Isar/expression.ML
changeset 47315 89a4bbf9790d
parent 47311 1addbe2a7458
child 49749 f27c96e98672
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 03 20:08:08 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 03 20:24:00 2012 +0200
     1.3 @@ -357,17 +357,19 @@
     1.4                Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
     1.5          val inst'' = map2 Type.constraint parm_types' inst';
     1.6          val insts' = insts @ [(loc, (prfx, inst''))];
     1.7 -        val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
     1.8 +        val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
     1.9          val inst''' = insts'' |> List.last |> snd |> snd;
    1.10          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
    1.11          val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
    1.12        in (i + 1, insts', ctxt'') end;
    1.13  
    1.14 -    fun prep_elem insts raw_elem (elems, ctxt) =
    1.15 +    fun prep_elem insts raw_elem ctxt =
    1.16        let
    1.17 -        val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
    1.18 -        val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
    1.19 -        val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
    1.20 +        val ctxt' = ctxt
    1.21 +          |> Context_Position.set_visible false
    1.22 +          |> declare_elem prep_vars_elem raw_elem
    1.23 +          |> Context_Position.restore_visible ctxt;
    1.24 +        val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
    1.25        in (elems', ctxt') end;
    1.26  
    1.27      fun prep_concl raw_concl (insts, elems, ctxt) =
    1.28 @@ -388,7 +390,7 @@
    1.29              commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
    1.30  
    1.31      val ctxt4 = init_body ctxt3;
    1.32 -    val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
    1.33 +    val (elems, ctxt5) = fold_map (prep_elem insts') raw_elems ctxt4;
    1.34      val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
    1.35  
    1.36      (* Retrieve parameter types *)