Mercurial Mercurial > hg > nominal2 / 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.
Quotient-Paper/Paper.thy
changeset 3111 60c4c93b30d5
parent 2811 9c2662447c30
child 3114 a9a4baa7779f 
--- a/Quotient-Paper/Paper.thy	Tue Jan 24 14:05:24 2012 +0000
+++ b/Quotient-Paper/Paper.thy	Tue Jan 24 14:29:07 2012 +0000
@@ -45,7 +45,7 @@
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   let
     val concl =
-      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
   in
     case concl of (_ $ l $ r) => proj (l, r)
     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
nominal2