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/Code_Evaluation.thy
changeset 33553 35f2b30593a8
parent 33473 3b275a0bf18c
child 33632 6ea8a4cce9e7 
--- a/src/HOL/Code_Evaluation.thy	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Tue Nov 10 16:04:57 2009 +0100
@@ -64,7 +64,7 @@
         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     in
       thy
-      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
+      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
       |> snd
isabelle