attribute where/of: proper Syntax.parse/check;
authorwenzelm
Wed Nov 07 16:43:01 2007 +0100 (2007-11-07)
changeset 2532963e8de11c8e9
parent 25328 f71105742e2c
child 25330 15bf0f47a87d
attribute where/of: proper Syntax.parse/check;
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Nov 07 16:43:00 2007 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed Nov 07 16:43:01 2007 +0100
     1.3 @@ -57,6 +57,18 @@
     1.4  
     1.5  in
     1.6  
     1.7 +fun read_termTs ctxt ss Ts =
     1.8 +  let
     1.9 +    fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
    1.10 +    val ts = map2 parse Ts ss;
    1.11 +    val ts' =
    1.12 +      map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
    1.13 +      |> Syntax.check_terms (ProofContext.set_mode ProofContext.mode_schematic ctxt)  (* FIXME !? *)
    1.14 +      |> Variable.polymorphic ctxt;
    1.15 +    val Ts' = map Term.fastype_of ts';
    1.16 +    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
    1.17 +  in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
    1.18 +
    1.19  fun read_insts ctxt mixed_insts (tvars, vars) =
    1.20    let
    1.21      val thy = ProofContext.theory_of ctxt;
    1.22 @@ -105,8 +117,7 @@
    1.23  
    1.24      val (xs, strs) = split_list external_insts;
    1.25      val Ts = map (the_type vars2) xs;
    1.26 -    val (ts, inferred) =   (* FIXME polymorphic!? schematic vs. 'for' context!? *)
    1.27 -      ProofContext.read_termTs_schematic ctxt (K false) (K NONE) (K NONE) [] (strs ~~ Ts);
    1.28 +    val (ts, inferred) = read_termTs ctxt strs Ts;
    1.29  
    1.30      val instT3 = Term.typ_subst_TVars inferred;
    1.31      val vars3 = map (apsnd instT3) vars2;