src/Pure/Proof/extraction.ML
changeset 33388 d64545e6cba5
parent 33337 9c3b9bf81e8b
child 33522 737589bb9bb8
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Nov 02 20:48:08 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Nov 02 20:50:48 2009 +0100
     1.3 @@ -300,7 +300,7 @@
     1.4      val rtypes = map fst types;
     1.5      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     1.6      val thy' = add_syntax thy;
     1.7 -    val rd = ProofSyntax.read_proof thy' false
     1.8 +    val rd = Proof_Syntax.read_proof thy' false;
     1.9    in fn (thm, (vs, s1, s2)) =>
    1.10      let
    1.11        val name = Thm.get_name thm;