more precise position information via Variable.add_fixes_binding;
authorwenzelm
Wed Apr 27 20:19:05 2011 +0200 (2011-04-27)
changeset 424914bb5de0aae66
parent 42490 3633ecaaf3ef
child 42492 83c57d850049
more precise position information via Variable.add_fixes_binding;
src/HOL/Tools/inductive.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Apr 27 19:55:42 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Apr 27 20:19:05 2011 +0200
     1.3 @@ -552,10 +552,10 @@
     1.4  val ind_cases_setup =
     1.5    Method.setup @{binding ind_cases}
     1.6      (Scan.lift (Scan.repeat1 Args.name_source --
     1.7 -      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
     1.8 +      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
     1.9        (fn (raw_props, fixes) => fn ctxt =>
    1.10          let
    1.11 -          val (_, ctxt') = Variable.add_fixes fixes ctxt;
    1.12 +          val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
    1.13            val props = Syntax.read_props ctxt' raw_props;
    1.14            val ctxt'' = fold Variable.declare_term props ctxt';
    1.15            val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 19:55:42 2011 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:19:05 2011 +0200
     2.3 @@ -1027,15 +1027,16 @@
     2.4  
     2.5  fun add_fixes raw_vars ctxt =
     2.6    let
     2.7 -    val (vars, _) = cert_vars raw_vars ctxt;
     2.8 -    val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt;
     2.9 -    val ctxt'' =
    2.10 -      ctxt'
    2.11 -      |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    2.12 -      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
    2.13 -    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    2.14 -      Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
    2.15 -  in (xs', ctxt'') end;
    2.16 +    val thy = theory_of ctxt;
    2.17 +    val vars = #1 (cert_vars raw_vars ctxt);
    2.18 +  in
    2.19 +    ctxt
    2.20 +    |> Variable.add_fixes_binding (map #1 vars)
    2.21 +    |-> (fn xs =>
    2.22 +      fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    2.23 +      #-> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed))
    2.24 +      #> pair xs)
    2.25 +  end;
    2.26  
    2.27  
    2.28  (* fixes vs. frees *)