changeset 42488 | 4638622bcaa1 |
parent 42361 | 23f352990944 |
child 45132 | 09de0d0de645 |
--- a/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 17:44:06 2011 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 17:58:45 2011 +0200 @@ -92,7 +92,7 @@ val finish_rule = split_all_tuples #> rename_params_rule true - (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding); + (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); fun rule_cases ctxt r = let val r' = if simp then Induct.simplified_rule ctxt r else r