src/Pure/Isar/element.ML
changeset 19897 fe661eb3b0e7
parent 19866 d47f32a4964a
child 19931 fb32b43e7f80
     1.1 --- a/src/Pure/Isar/element.ML	Thu Jun 15 18:35:16 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Jun 15 23:08:54 2006 +0200
     1.3 @@ -214,10 +214,10 @@
     1.4  
     1.5  fun obtain prop ctxt =
     1.6    let
     1.7 -    val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop);
     1.8 +    val xs = Variable.rename_wrt ctxt [] (Logic.strip_params prop);
     1.9      val args = rev (map Free xs);
    1.10      val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t));
    1.11 -    val ctxt' = ctxt |> fold ProofContext.declare_term args;
    1.12 +    val ctxt' = ctxt |> fold Variable.declare_term args;
    1.13    in (("", (map (apsnd SOME) xs, As)), ctxt') end;
    1.14  
    1.15  in
    1.16 @@ -235,12 +235,12 @@
    1.17  
    1.18      val raw_prop =
    1.19        Thm.prop_of th
    1.20 -      |> singleton (ProofContext.monomorphic ctxt)
    1.21 +      |> singleton (Variable.monomorphic ctxt)
    1.22        |> K (ObjectLogic.is_elim th) ? standard_thesis
    1.23        |> Term.zero_var_indexes;
    1.24  
    1.25      val vars = Term.add_vars raw_prop [];
    1.26 -    val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
    1.27 +    val frees = Variable.rename_wrt ctxt [raw_prop] (map (apfst fst) vars);
    1.28      val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees);
    1.29  
    1.30      val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
    1.31 @@ -252,7 +252,7 @@
    1.32      pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
    1.33      pretty_stmt ctxt
    1.34       (if null cases then Shows [(("", []), [(concl, [])])]
    1.35 -      else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
    1.36 +      else Obtains (#1 (fold_map obtain cases (ctxt |> Variable.declare_term prop))))
    1.37    end |> thm_name kind raw_th;
    1.38  
    1.39  end;