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/HOL/Statespace/state_space.ML
changeset 41270 dea60d052923
parent 39134 917b4b6ba3d2
child 41472 f6ab14e61604 
--- a/src/HOL/Statespace/state_space.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -145,7 +145,7 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_cmd name expr
+   |> Expression.sublocale_cmd name expr []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> ProofContext.theory_of
isabelle