src/Pure/Isar/proof_context.ML
changeset 28941 128459bd72d2
parent 28864 d6fe93e3dcb9
child 28965 1de908189869
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -971,7 +971,7 @@
     1.4  
     1.5  fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
     1.6    let
     1.7 -    val pos = Name.pos_of b;
     1.8 +    val pos = Binding.pos_of b;
     1.9      val name = full_binding ctxt b;
    1.10      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
    1.11  
    1.12 @@ -1128,7 +1128,7 @@
    1.13        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    1.14        |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    1.15      val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    1.16 -      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
    1.17 +      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
    1.18    in (xs', ctxt'') end;
    1.19  
    1.20  in