# HG changeset patch # User Christian Urban # Date 1335797123 -3600 # Node ID 31c64dd4c95a3f7a6ab6755c92062ecf4afab0fb # Parent 603a36f19bfe66b8e72d048f0539a169fcc5ae9a adapted to change by Markus on function.ML diff -r 603a36f19bfe -r 31c64dd4c95a Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Thu Apr 19 15:39:46 2012 +0100 +++ b/Nominal/nominal_function.ML Mon Apr 30 15:45:23 2012 +0100 @@ -245,7 +245,6 @@ (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) "declaration of congruence rule for function definitions" #> setup_case_cong - #> Function_Relation.setup #> Function_Common.Termination_Simps.setup val get_congs = Function_Ctx_Tree.get_function_congs