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/rule_insts.ML
changeset 21879 a3efbae45735
parent 21500 146938537ddc
child 22681 9d42e5365ad1 
--- a/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -349,7 +349,7 @@
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args f src ctxt =
-  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
+  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
 
 val insts_var =
   Scan.optional
@@ -357,7 +357,7 @@
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args_var f src ctxt =
-  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
+  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
 
 
 (* setup *)
isabelle