more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
authorwenzelm
Wed Apr 27 19:55:42 2011 +0200 (2011-04-27)
changeset 424903633ecaaf3ef
parent 42489 db9b9e46131c
child 42491 4bb5de0aae66
more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Apr 27 19:39:50 2011 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 19:55:42 2011 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5      (*obtain vars*)
     1.6      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     1.7 -    val (_, fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
     1.8 +    val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
     1.9      val xs = map (Variable.name o #1) vars;
    1.10  
    1.11      (*obtain asms*)
    1.12 @@ -126,17 +126,15 @@
    1.13      val asm_props = maps (map fst) proppss;
    1.14      val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
    1.15  
    1.16 -    val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
    1.17 +    (*obtain parms*)
    1.18 +    val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
    1.19 +    val parms = xs' ~~ Ts;
    1.20 +    val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
    1.21  
    1.22      (*obtain statements*)
    1.23      val thesisN = Name.variant xs Auto_Bind.thesisN;
    1.24      val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
    1.25  
    1.26 -    val asm_frees = fold Term.add_frees asm_props [];
    1.27 -    val parms = xs |> map (fn x =>
    1.28 -      let val x' = Variable.intern_fixed fix_ctxt x
    1.29 -      in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
    1.30 -
    1.31      val that_name = if name = "" then thatN else name;
    1.32      val that_prop =
    1.33        Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))