src/Pure/Isar/local_defs.ML
changeset 19897 fe661eb3b0e7
parent 19585 70a1ce3b23ae
child 20021 815393c02db9
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Jun 15 18:35:16 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Jun 15 23:08:54 2006 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4      fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
     1.5      val ((lhs, _), eq') = eq
     1.6        |> Sign.no_vars pp
     1.7 -      |> Logic.dest_def pp Term.is_Free (ProofContext.is_fixed ctxt) (K true)
     1.8 +      |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
     1.9        handle TERM (msg, _) => err msg | ERROR msg => err msg;
    1.10    in (Term.dest_Free (Term.head_of lhs), eq') end;
    1.11  
    1.12 @@ -157,7 +157,7 @@
    1.13          val thy' = ProofContext.theory_of ctxt';
    1.14          val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
    1.15          val frees = Term.fold_aterms (fn Free (x, _) =>
    1.16 -          if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    1.17 +          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    1.18        in
    1.19          Goal.prove thy' frees [] prop' (K (ALLGOALS
    1.20            (meta_rewrite_tac ctxt' THEN'