src/Pure/Isar/obtain.ML
changeset 19897 fe661eb3b0e7
parent 19844 2c1fdc397ded
child 19906 c23a0e65b285
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Jun 15 18:35:16 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jun 15 23:08:54 2006 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4      val asm_props = maps (map fst) proppss;
     1.5      val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
     1.6  
     1.7 -    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
     1.8 +    val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
     1.9  
    1.10      (*obtain statements*)
    1.11      val thesisN = Term.variant xs AutoBind.thesisN;
    1.12 @@ -220,7 +220,7 @@
    1.13    in ((x, T, mx), ctxt') end;
    1.14  
    1.15  fun polymorphic (vars, ctxt) =
    1.16 -  let val Ts = map Logic.dest_type (ProofContext.polymorphic ctxt (map (Logic.mk_type o #2) vars))
    1.17 +  let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
    1.18    in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;
    1.19  
    1.20  fun gen_guess prep_vars raw_vars int state =
    1.21 @@ -308,7 +308,7 @@
    1.22              val props = map fst propp;
    1.23              val (parms, ctxt'') =
    1.24                ctxt'
    1.25 -              |> fold ProofContext.declare_term props
    1.26 +              |> fold Variable.declare_term props
    1.27                |> fold_map ProofContext.inferred_param xs;
    1.28              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    1.29            in