Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/method.ML
changeset 36096 abc6a2ea4b88
parent 36093 0880493627ca
parent 35625 9c818cab0dd0
child 36950 75b8f26f2f07 
--- a/src/Pure/Isar/method.ML	Fri Apr 02 13:33:48 2010 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 07 19:17:10 2010 +0200
@@ -166,14 +166,14 @@
 
 (* unfold/fold definitions *)
 
-fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.unfold_tac ctxt ths));
-fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.fold_tac ctxt ths));
+fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths));
+fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths));
 
 
 (* atomize rule statements *)
 
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
-  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
+  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
 
 
 (* this -- resolve facts directly *)
isabelle