src/Pure/Isar/obtain.ML
changeset 47815 43f677b3ae91
parent 46728 85f8e3932712
child 49660 de49d9b4d7bc
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4      val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
     1.5      val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
     1.6      val asm_props = maps (map fst) proppss;
     1.7 -    val asms = map fst (Attrib.map_specs (map (prep_att thy)) raw_asms) ~~ proppss;
     1.8 +    val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss;
     1.9  
    1.10      (*obtain parms*)
    1.11      val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
    1.12 @@ -168,7 +168,7 @@
    1.13  in
    1.14  
    1.15  val obtain = gen_obtain (K I) Proof_Context.cert_vars Proof_Context.cert_propp;
    1.16 -val obtain_cmd = gen_obtain Attrib.attribute Proof_Context.read_vars Proof_Context.read_propp;
    1.17 +val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.read_propp;
    1.18  
    1.19  end;
    1.20