src/HOLCF/Tools/pcpodef_package.ML
changeset 24867 e5b55d7be9bb
parent 24712 64ed05609568
child 24920 2a45e400fdad
     1.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -(* copied from HOL/Tools/typedef_package.ML *)
     1.8 +(* cf. HOL/Tools/typedef_package.ML *)
     1.9  val typedef_proof_decl =
    1.10    Scan.optional (P.$$$ "(" |--
    1.11        ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
    1.12 @@ -196,18 +196,16 @@
    1.13    (if pcpo then pcpodef_proof else cpodef_proof)
    1.14      ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
    1.15  
    1.16 -val pcpodefP =
    1.17 +val _ =
    1.18    OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
    1.19      (typedef_proof_decl >>
    1.20        (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
    1.21  
    1.22 -val cpodefP =
    1.23 +val _ =
    1.24    OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
    1.25      (typedef_proof_decl >>
    1.26        (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
    1.27  
    1.28 -val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
    1.29 -
    1.30  end;
    1.31  
    1.32  end;