# HG changeset patch
# User haftmann
# Date 1289989599 -3600
# Node ID 6fed6f9464717a1939b3511edc3f7462191d189e
# Parent  968c481aa18ce10a265fd8010dbe3c674e4589e4
stub for Isar command interface

diff -r 968c481aa18c -r 6fed6f946471 src/HOL/Tools/functorial_mappers.ML
--- a/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:09:18 2010 +0100
+++ b/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:26:39 2010 +0100
@@ -147,4 +147,21 @@
         concatenate = concatenate, identity = identity }))
   end;
 
+fun gen_type_mapper prep_term raw_t thy =
+  let
+    val t = prep_term thy raw_t;
+    val after_qed = K I;
+  in
+    thy
+    |> Named_Target.theory_init
+    |> Proof.theorem NONE after_qed []
+  end
+
+val type_mapper = gen_type_mapper Sign.cert_term;
+val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
+
+val _ =
+  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
+    (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
+
 end;